[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

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

lemma "G â H â example G â example H"
  fix x :: "nat"
  assume "G â H â x â example G"
  hence "x â example H"

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
  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.


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