# HG changeset patch
# User wenzelm
# Date 1564405830 -7200
# Node ID 145fb19d906d29464f2559ce69c681fe9adcfb96
# Parent  99024c9c83f69330e00a73dd37ce997e46349814
tuned -- non-strict args;

diff -r 99024c9c83f6 -r 145fb19d906d src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Jul 29 11:38:05 2019 +0200
+++ b/src/Pure/proofterm.ML	Mon Jul 29 15:10:30 2019 +0200
@@ -1710,8 +1710,6 @@
     val args = prop_args prop;
 
     val (ucontext, prop1) = Logic.unconstrainT shyps prop;
-    val args1 = (map o Option.map o Term.map_types) (#map_atyps ucontext) args;
-    val argsP = map OfClass (#outer_constraints ucontext) @ map Hyp hyps;
 
     val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
     val body0 =
@@ -1741,9 +1739,11 @@
 
     val head = PThm (i, ((name, prop1, NONE, open_proof), body'));
     val proof =
-      if unconstrain
-      then proof_combt' (head, args1)
-      else proof_combP (proof_combt' (head, args), argsP);
+      if unconstrain then
+        proof_combt' (head, (map o Option.map o Term.map_types) (#map_atyps ucontext) args)
+      else
+        proof_combP (proof_combt' (head, args),
+          map OfClass (#outer_constraints ucontext) @ map Hyp hyps);
   in (pthm, proof) end;
 
 in