--- a/src/Tools/induct_tacs.ML Fri Nov 26 22:04:33 2010 +0100
+++ b/src/Tools/induct_tacs.ML Fri Nov 26 22:29:41 2010 +0100
@@ -96,7 +96,7 @@
val _ = Method.trace ctxt [rule'];
val concls = Logic.dest_conjunctions (Thm.concl_of rule);
- val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
+ val insts = maps prep_inst (concls ~~ varss) handle ListPair.UnequalLengths =>
error "Induction rule has different numbers of variables";
in res_inst_tac ctxt insts rule' i st end
handle THM _ => Seq.empty;