[isabelle-dev] Fwd: [isabelle] Exception in conv.ML

[Lawrence Paulson]

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.