# HG changeset patch
# User wenzelm
# Date 1704543228 -3600
# Node ID 16c65e67dd754bb1dcf93a1a5dd3ac21867b0ff7
# Parent  84154518026947743a02c355e53931e2e344bdba
misc tuning and clarification;

diff -r 841545180269 -r 16c65e67dd75 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Jan 06 12:44:35 2024 +0100
+++ b/src/Pure/proofterm.ML	Sat Jan 06 13:13:48 2024 +0100
@@ -2236,14 +2236,16 @@
 
     val header = thm_header i ([pos, Position.thread_data ()]) theory_name name prop1 NONE;
     val head = PThm (header, Thm_Body {open_proof = open_proof, body = thm_body});
-    val proof2 =
+    val argst =
       if unconstrain then
-        proof_combt' (head,
-          (Same.commit o Same.map o Same.map_option o Term.map_types_same)
-            (typ_operation {strip_sorts = true}) args)
-      else
-        proof_combP (proof_combt' (head, args),
-          map PClass (#outer_constraints ucontext) @ map Hyp hyps);
+        (Same.commit o Same.map o Same.map_option o Term.map_types_same)
+          (typ_operation {strip_sorts = true}) args
+      else args;
+    val argsP =
+      if unconstrain then []
+      else map PClass (#outer_constraints ucontext) @ map Hyp hyps;
+    val proof2 = proof_combP (proof_combt' (head, argst), argsP);
+
     val (zboxes2, zproof2) =
       if unconstrain then (zboxes1, zproof1)  (* FIXME proper zproof *)
       else (zboxes1, zproof1);