# HG changeset patch
# User wenzelm
# Date 1564235425 -7200
# Node ID da89a7768a4a16d3a7d3decd3b49a6951e7e6ddb
# Parent  d6a5301f9ffb6f404247e5f1483d603a7827c8a3
tuned;

diff -r d6a5301f9ffb -r da89a7768a4a src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Jul 27 15:24:16 2019 +0200
+++ b/src/Pure/proofterm.ML	Sat Jul 27 15:50:25 2019 +0200
@@ -1712,7 +1712,7 @@
   if Options.default_bool "prune_proofs" then MinProof
   else shrink_proof proof;
 
-fun prepare_thm_proof thy name shyps hyps concl promises body =
+fun prepare_thm_proof unconstrain thy name shyps hyps concl promises body =
   let
     val named = name <> "";
 
@@ -1744,23 +1744,26 @@
       (*non-deterministic, depends on unknown promises*)
       (case strip_combt (fst (strip_combP prf)) of
         (PThm (i, ((a, prop', NONE, _), body')), args') =>
-          if (a = "" orelse a = name) andalso prop1 = prop' andalso args = args'
+          if (a = "" orelse a = name) andalso prop' = prop1 andalso args' = args
           then (i, body' |> (a = "" andalso named) ? Future.map (publish i))
           else new_prf ()
       | _ => new_prf ());
 
+    val pthm = (i, make_thm_node name prop1 body');
+
     val head = PThm (i, ((name, prop1, NONE, open_proof), body'));
-  in ((i, make_thm_node name prop1 body'), head, args, argsP, args1) end;
+    val proof =
+      if unconstrain
+      then proof_combt' (head, args1)
+      else proof_combP (proof_combt' (head, args), argsP);
+  in (pthm, proof) end;
 
 in
 
-fun thm_proof thy name shyps hyps concl promises body =
-  let val (pthm, head, args, argsP, _) = prepare_thm_proof thy name shyps hyps concl promises body
-  in (pthm, proof_combP (proof_combt' (head, args), argsP)) end;
+val thm_proof = prepare_thm_proof false;
 
 fun unconstrain_thm_proof thy shyps concl promises body =
-  let val (pthm, head, _, _, args) = prepare_thm_proof thy "" shyps [] concl promises body
-  in (pthm, proof_combt' (head, args)) end;
+  prepare_thm_proof true thy "" shyps [] concl promises body;
 
 end;