# HG changeset patch
# User wenzelm
# Date 1570652303 -7200
# Node ID 3ae7949ef05903c78682e27d5cd0cc01a6c10578
# Parent  785a2112f86106bcb824228813c0b74d373e1c2e
tuned -- allow slightly more expensive atomic proofs;

diff -r 785a2112f861 -r 3ae7949ef059 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Oct 09 21:59:56 2019 +0200
+++ b/src/Pure/thm.ML	Wed Oct 09 22:18:23 2019 +0200
@@ -729,7 +729,10 @@
   in make_deriv ps oracles thms prf end;
 
 fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
-fun deriv_rule0 prf = deriv_rule1 I (make_deriv [] [] [] prf);
+
+fun deriv_rule0 make_prf =
+  if ! Proofterm.proofs <= 1 then empty_deriv
+  else deriv_rule1 I (make_deriv [] [] [] (make_prf ()));
 
 fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) =
   make_deriv promises oracles thms (f proof);
@@ -803,7 +806,7 @@
       Name_Space.lookup (Theory.axiom_table thy) name
       |> Option.map (fn prop =>
            let
-             val der = deriv_rule0 (Proofterm.axm_proof name prop);
+             val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop);
              val cert = Context.Certificate thy;
              val maxidx = maxidx_of_term prop;
              val shyps = Sorts.insert_term prop [];
@@ -1078,7 +1081,7 @@
       raise THM ("assume: prop", 0, [])
     else if maxidx <> ~1 then
       raise THM ("assume: variables", maxidx, [])
-    else Thm (deriv_rule0 (Proofterm.Hyp prop),
+    else Thm (deriv_rule0 (fn () => Proofterm.Hyp prop),
      {cert = cert,
       tags = [],
       maxidx = ~1,
@@ -1205,7 +1208,7 @@
   t \<equiv> t
 *)
 fun reflexive (Cterm {cert, t, T = _, maxidx, sorts}) =
-  Thm (deriv_rule0 Proofterm.reflexive,
+  Thm (deriv_rule0 (fn () => Proofterm.reflexive),
    {cert = cert,
     tags = [],
     maxidx = maxidx,
@@ -1274,7 +1277,7 @@
       (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt)
       | _ => raise THM ("beta_conversion: not a redex", 0, []));
   in
-    Thm (deriv_rule0 Proofterm.reflexive,
+    Thm (deriv_rule0 (fn () => Proofterm.reflexive),
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -1286,7 +1289,7 @@
   end;
 
 fun eta_conversion (Cterm {cert, t, T = _, maxidx, sorts}) =
-  Thm (deriv_rule0 Proofterm.reflexive,
+  Thm (deriv_rule0 (fn () => Proofterm.reflexive),
    {cert = cert,
     tags = [],
     maxidx = maxidx,
@@ -1297,7 +1300,7 @@
     prop = Logic.mk_equals (t, Envir.eta_contract t)});
 
 fun eta_long_conversion (Cterm {cert, t, T = _, maxidx, sorts}) =
-  Thm (deriv_rule0 Proofterm.reflexive,
+  Thm (deriv_rule0 (fn () => Proofterm.reflexive),
    {cert = cert,
     tags = [],
     maxidx = maxidx,
@@ -1628,7 +1631,7 @@
   if T <> propT then
     raise THM ("trivial: the term must have type prop", 0, [])
   else
-    Thm (deriv_rule0 (Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)),
+    Thm (deriv_rule0 (fn () => Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)),
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -1652,7 +1655,7 @@
     val Cterm {t = prop, maxidx, sorts, ...} = global_cterm_of thy (Logic.mk_of_class (T, c));
   in
     if Sign.of_sort thy (T, [c]) then
-      Thm (deriv_rule0 (Proofterm.OfClass (T, c)),
+      Thm (deriv_rule0 (fn () => Proofterm.OfClass (T, c)),
        {cert = cert,
         tags = [],
         maxidx = maxidx,