[isabelle-dev] Interrupt exception

[Lucas Dixon]

Using the development version of Isabelle (1d4d0b305f16),
I just noticed a strange exception being raised...

theory norm
imports Complex_Main
begin

fun internalise where
     intern_base: "internalise 0 (a,l) = (a, l)"
   | intern_step: "internalise (Suc n) (a,l) = internalise n (Suc a, l)"

fun extr where "extr (a,l) = foldr (op +) l a"

lemma [simp]: "internalise 0 x = x" by (induct x, simp_all)
lemma [simp]: "foldr (op +) l (Suc a) = Suc (foldr (op +) l a)"
by (induct l, simp_all)
lemma [simp]: "internalise (Suc n) (internalise m (a, l))
   = internalise n (internalise m (Suc a,l))"
   by (induct m arbitrary: a, simp_all)

theorem case1: "internalise (n + m) al = internalise n (internalise m al)"
   apply (unfold Product_Type.pair_collapse[symmetric, of "al"])

this gives me:

*** Interrupt.
*** At command "apply".

Interrupt: script management may be in an inconsistent state
            (but it's probably okay)

That's probably not the way it is supposed to fail...
(I'm using ProofGeneral 3.7.1)

best,
lucas

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.