--- a/src/Pure/Proof/reconstruct.ML Wed Oct 21 12:02:19 2009 +0200
+++ b/src/Pure/Proof/reconstruct.ML Wed Oct 21 12:02:56 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, union (op =)
+ 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 _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");