diff -r 69e29cf993c0 -r caddb5264048 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Wed Aug 10 19:45:57 2011 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Wed Aug 10 19:46:48 2011 +0200
@@ -288,9 +288,9 @@
     val _ = message "Collecting constraints...";
     val (t, prf, cs, env, _) = make_constraints_cprf thy
       (Envir.empty (Proofterm.maxidx_proof cprf ~1)) cprf';
-    val cs' = map (fn p => (true, p, uncurry (union (op =)) 
-        (pairself (map (fst o dest_Var) o OldTerm.term_vars) p)))
-      (map (pairself (Envir.norm_term env)) ((t, prop')::cs));
+    val cs' =
+      map (pairself (Envir.norm_term env)) ((t, prop') :: cs)
+      |> map (fn p => (true, p, Term.add_var_names (#1 p) (Term.add_var_names (#2 p) [])));
     val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");
     val env' = solve thy cs' env
   in