--- a/src/Pure/Proof/reconstruct.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/Proof/reconstruct.ML Tue Oct 20 16:13:01 2009 +0200
@@ -289,7 +289,7 @@
val _ = message "Collecting constraints...";
val (t, prf, cs, env, _) = make_constraints_cprf thy
(Envir.empty (maxidx_proof cprf ~1)) cprf';
- val cs' = map (fn p => (true, p, op union
+ val cs' = map (fn p => (true, p, gen_union (op =)
(pairself (map (fst o dest_Var) o OldTerm.term_vars) p)))
(map (pairself (Envir.norm_term env)) ((t, prop')::cs));
val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");