# HG changeset patch
# User wenzelm
# Date 1566293309 -7200
# Node ID 729f4d066d1aa8097a1263c08cb1793e7db35e6c
# Parent  57df8a85317a5160e15a19d9306fa56261ef64ca
tuned;

diff -r 57df8a85317a -r 729f4d066d1a src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Aug 20 11:01:05 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Aug 20 11:28:29 2019 +0200
@@ -8,11 +8,11 @@
 
 signature PROOFTERM =
 sig
-  type thm_node
   type thm_header =
     {serial: serial, pos: Position.T list, theory_name: string, name: string,
       prop: term, types: typ list option}
   type thm_body
+  type thm_node
   datatype proof =
      MinProof
    | PBound of int
@@ -29,12 +29,11 @@
     {oracles: (string * term option) Ord_List.T,
      thms: (serial * thm_node) Ord_List.T,
      proof: proof}
-  val %> : proof * term -> proof
-  val proofs: int Unsynchronized.ref
+  type oracle = string * term option
+  type pthm = serial * thm_node
   exception MIN_PROOF
-  type pthm = serial * thm_node
-  type oracle = string * term option
   val proof_of: proof_body -> proof
+  val join_proof: proof_body future -> proof
   val map_proof_of: (proof -> proof) -> proof_body -> proof_body
   val thm_header: serial -> Position.T list -> string -> string -> term -> typ list option ->
     thm_header
@@ -44,13 +43,11 @@
   val thm_node_name: thm_node -> string
   val thm_node_prop: thm_node -> term
   val thm_node_body: thm_node -> proof_body future
-  val join_proof: proof_body future -> proof
+  val consolidate: proof_body list -> unit
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   val fold_body_thms:
     ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
     proof_body list -> 'a -> 'a
-  val consolidate: proof_body list -> unit
-
   val oracle_ord: oracle ord
   val thm_ord: pthm ord
   val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
@@ -67,7 +64,10 @@
   val decode: proof XML.Decode.T
   val decode_body: proof_body XML.Decode.T
 
+  val %> : proof * term -> proof
+
   (*primitive operations*)
+  val proofs: int Unsynchronized.ref
   val proofs_enabled: unit -> bool
   val atomic_proof: proof -> bool
   val compact_proof: proof -> bool
@@ -204,13 +204,14 @@
 and thm_node =
   Thm_Node of {name: string, prop: term, body: proof_body future, consolidate: unit lazy};
 
-exception MIN_PROOF;
-
 type oracle = string * term option;
 val oracle_prop = the_default Term.dummy;
 
 type pthm = serial * thm_node;
 
+exception MIN_PROOF;
+
+
 fun proof_of (PBody {proof, ...}) = proof;
 val join_proof = Future.join #> proof_of;
 
@@ -429,6 +430,9 @@
 
 (** proof objects with different levels of detail **)
 
+val proofs = Unsynchronized.ref 2;
+fun proofs_enabled () = ! proofs >= 2;
+
 fun atomic_proof prf =
   (case prf of
     Abst _ => false
@@ -1086,9 +1090,6 @@
 
 (** axioms and theorems **)
 
-val proofs = Unsynchronized.ref 2;
-fun proofs_enabled () = ! proofs >= 2;
-
 fun vars_of t = map Var (rev (Term.add_vars t []));
 fun frees_of t = map Free (rev (Term.add_frees t []));
 
diff -r 57df8a85317a -r 729f4d066d1a src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Aug 20 11:01:05 2019 +0200
+++ b/src/Pure/thm.ML	Tue Aug 20 11:28:29 2019 +0200
@@ -933,7 +933,7 @@
 fun union_digest (oracles1, thms1) (oracles2, thms2) =
   (Proofterm.unions_oracles [oracles1, oracles2], Proofterm.unions_thms [thms1, thms2]);
 
-fun thm_digest (Thm (Deriv {body = Proofterm.PBody {oracles, thms, ...}, ...}, _)) =
+fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) =
   (oracles, thms);
 
 fun constraint_digest ({theory = thy, typ, sort, ...}: constraint) =
@@ -963,10 +963,10 @@
             raise THEORY ("solve_constraints: bad theories for theorem\n" ^
               Syntax.string_of_term_global thy (prop_of thm), thy :: bad_thys);
 
-        val Deriv {promises, body = Proofterm.PBody {oracles, thms, proof}} = der;
+        val Deriv {promises, body = PBody {oracles, thms, proof}} = der;
         val (oracles', thms') = (oracles, thms)
           |> fold (fold union_digest o constraint_digest) constraints;
-        val body' = Proofterm.PBody {oracles = oracles', thms = thms', proof = proof};
+        val body' = PBody {oracles = oracles', thms = thms', proof = proof};
       in
         Thm (Deriv {promises = promises, body = body'},
           {constraints = [], cert = cert, tags = tags, maxidx = maxidx,