# HG changeset patch
# User wenzelm
# Date 1570815359 -7200
# Node ID 2d991e01a6712b77f941d76a35edba07341f72bc
# Parent  614ca81fa28e53dd7409dd0accccd645987600f9
proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g. relevant for proof reconstruction of List.list.full_exhaustive_list.simps;

diff -r 614ca81fa28e -r 2d991e01a671 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Oct 11 18:26:35 2019 +0200
+++ b/src/Pure/proofterm.ML	Fri Oct 11 19:35:59 2019 +0200
@@ -143,7 +143,6 @@
     (string * class list list * class -> proof) ->
     (typ * class -> proof) -> typ * sort -> proof list
   val axm_proof: string -> term -> proof
-  val make_oracle: string -> term -> oracle
   val oracle_proof: string -> term -> proof
   val shrink_proof: proof -> proof
 
@@ -1165,14 +1164,15 @@
     val frees = map SOME (frees_of prop);
   in vars @ frees end;
 
-fun axm_proof name prop =
-  proof_combt' (PAxm (name, prop, NONE), prop_args prop);
+fun const_proof mk name prop =
+  let
+    val args = prop_args prop;
+    val ({outer_constraints, ...}, prop1) = Logic.unconstrainT [] prop;
+    val head = mk (name, prop1, NONE);
+  in proof_combP (proof_combt' (head, args), map OfClass outer_constraints) end;
 
-fun make_oracle name prop : oracle =
-  if ! proofs = 0 then (name, NONE) else (name, SOME prop);
-
-fun oracle_proof name prop =
-  proof_combt' (Oracle (name, prop, NONE), prop_args prop);
+val axm_proof = const_proof PAxm;
+val oracle_proof = const_proof Oracle;
 
 val shrink_proof =
   let
diff -r 614ca81fa28e -r 2d991e01a671 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Oct 11 18:26:35 2019 +0200
+++ b/src/Pure/thm.ML	Fri Oct 11 19:35:59 2019 +0200
@@ -713,6 +713,9 @@
 
 val promise_ord: (serial * thm future) ord = fn ((i, _), (j, _)) => int_ord (j, i);
 
+fun bad_proofs i =
+  error ("Illegal level of detail for proof objects: " ^ string_of_int i);
+
 fun deriv_rule2 f
     (Deriv {promises = ps1, body = PBody {oracles = oracles1, thms = thms1, proof = prf1}})
     (Deriv {promises = ps2, body = PBody {oracles = oracles2, thms = thms2, proof = prf2}}) =
@@ -725,7 +728,7 @@
         2 => f prf1 prf2
       | 1 => MinProof
       | 0 => MinProof
-      | i => error ("Illegal level of detail for proof objects: " ^ string_of_int i));
+      | i => bad_proofs i);
   in make_deriv ps oracles thms prf end;
 
 fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
@@ -1044,8 +1047,12 @@
           raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
         else
           let
-            val oracle = Proofterm.make_oracle name prop;
-            val prf = if ! Proofterm.proofs = 2 then Proofterm.oracle_proof name prop else MinProof;
+            val (oracle, prf) =
+              (case ! Proofterm.proofs of
+                2 => ((name, SOME prop), Proofterm.oracle_proof name prop)
+              | 1 => ((name, SOME prop), MinProof)
+              | 0 => ((name, NONE), MinProof)
+              | i => bad_proofs i);
           in
             Thm (make_deriv [] [oracle] [] prf,
              {cert = Context.join_certificate (Context.Certificate thy', cert2),