# HG changeset patch
# User wenzelm
# Date 1141839448 -3600
# Node ID 111ba44c66b2c01622ae21650e1085bcebc43c27
# Parent  aab0c0399e91b7a0bede6fbd504e337f7642b05d
infer_derivs: avoid allocating empty MinProof;

diff -r aab0c0399e91 -r 111ba44c66b2 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Mar 08 18:37:27 2006 +0100
+++ b/src/Pure/proofterm.ML	Wed Mar 08 18:37:28 2006 +0100
@@ -204,16 +204,19 @@
   error ("Illegal level of detail for proof objects: " ^ string_of_int i);
 
 fun if_ora b = if b then oracles_of_proof else K;
+val min_proof = MinProof ([], [], []);
 
 fun infer_derivs f (ora1, prf1) (ora2, prf2) =
-  (ora1 orelse ora2, 
-   case !proofs of
-     2 => f prf1 prf2
-   | 1 => MinProof (([], [], []) |> mk_min_proof prf1 |> mk_min_proof prf2)
-   | 0 => MinProof ([], [], if_ora ora2 (if_ora ora1 [] prf1) prf2)
-   | i => err_illegal_level i);
+  let val ora = ora1 orelse ora2 in
+    (ora,
+      case !proofs of
+        2 => f prf1 prf2
+      | 1 => MinProof (([], [], []) |> mk_min_proof prf1 |> mk_min_proof prf2)
+      | 0 => if ora then MinProof ([], [], if_ora ora2 (if_ora ora1 [] prf1) prf2) else min_proof
+      | i => err_illegal_level i)
+  end;
 
-fun infer_derivs' f = infer_derivs (K f) (false, MinProof ([], [], []));
+fun infer_derivs' f = infer_derivs (K f) (false, min_proof);
 
 fun (prf %> t) = prf % SOME t;