src/Pure/Proof/reconstruct.ML

   let
     val (cprf' % SOME prop', thawf) = freeze_thaw_prf (cprf % SOME prop);
     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') ^ ") ...");
     val env' = solve thy cs' env
   in