[isabelle] exception UnequalLengths raised (line 543 of "library.ML")



I was following along in the case study in tutorial.pdf and I got an
exception while writing my proof. I'm using Isabelle2015 on windows.

Here is a (slightly) simplified version of what I was doing that raised the
exception:

inductive_set
  example :: "nat set â nat set"
  for H   :: "nat set"
  where
    Inj [intro,simp] : "X â H â X â example H"
  | Fst:   "X â example H â X â example H"

lemma "G â H â example G â example H"
proof
  fix x :: "nat"
  assume "G â H â x â example G"
  hence "x â example H"
  proof(induction)


The line "proof(induction)" generates the following:
proof (prove): depth 1

using this:
  (Gânat set) â (Hânat set) â (xânat) â example G

goal (1 subgoal):
 1. x â example H
variables:
  H :: nat set
  x :: nat
exception UnequalLengths raised (line 543 of "library.ML")


Is this a normal error message or does it indicate some problem inside
Isabelle (eg., something I should be reporting)? If you delete the "Fst"
constructor the exception goes away.

Thanks,
Jason



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.