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
end
| 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.
Larry
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.
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
