# 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;