diff -r e5089e903e39 -r 441260986b63 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Fri Nov 26 22:04:33 2010 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Fri Nov 26 22:29:41 2010 +0100
@@ -137,7 +137,7 @@
                 NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env
               | SOME Ts => (Ts, env));
             val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
-              (forall_intr_vfs prop) handle Library.UnequalLengths =>
+              (forall_intr_vfs prop) handle ListPair.UnequalLengths =>
                 error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf))
           in (prop', Proofterm.change_type (SOME Ts) prf, [], env', vTs) end;