[isabelle-dev] Fwd: [isabelle] Exception in conv.ML
lp15 at cam.ac.uk
Thu Jun 9 16:43:09 CEST 2011
I see you are alert, as always!
In this particular case, it's pretty clear that the exception was raised here, in conv.ML:
fun gconv_rule cv i th =
(case try (Thm.cprem_of th) i of
SOME ct =>
let val eq = cv ct in
if Thm.is_reflexive eq then th
else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th
| NONE => raise THM ("gconv_rule", i, [th]));
And this was in conformance with a common use of exception THM, namely to indicate that the designated subgoal did not exist. So a tactic calling this code should indeed catch the exception and indicate failure by returning the empty sequence.
On 9 Jun 2011, at 13:29, Makarius wrote:
> Did anybody actually understand the source of the problem? The changelog of c46107e6714b claims a "fix" without any explanation what was broken. A spurious THM exception could have a quite unexpected cause.
More information about the isabelle-dev