# HG changeset patch
# User wenzelm
# Date 1566305727 -7200
# Node ID 00b67aaa4010a5152f4a8d82bfb6c4da27c263ef
# Parent  35a4ef9c6d8094b3ae89aa471daca948d5de8875
clarified modules;

diff -r 35a4ef9c6d80 -r 00b67aaa4010 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Aug 20 11:38:48 2019 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Aug 20 14:55:27 2019 +0200
@@ -173,6 +173,21 @@
     val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
   in parse ctxt' s |> Type.constraint T |> Syntax.check_term ctxt' end;
 
+fun make_proof_body prf =
+  let
+    val (oracles, thms) =
+      ([prf], ([], [])) |-> Proofterm.fold_proof_atoms false
+        (fn Oracle (name, prop, _) => apfst (cons (name, prop))
+          | PThm (header, thm_body) => apsnd (cons (Proofterm.make_thm header thm_body))
+          | _ => I);
+    val body =
+      PBody
+       {oracles = Ord_List.make Proofterm.oracle_ord oracles,
+        thms = Ord_List.make Proofterm.thm_ord thms,
+        proof = prf};
+  in Proofterm.thm_body body end;
+
+
 
 (**** theory data ****)
 
@@ -625,11 +640,10 @@
                       Proofterm.thm_header (serial ()) pos theory_name
                         (corr_name name vs') corr_prop
                         (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
-                    val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf);
                     val corr_prf' =
                       Proofterm.proof_combP
                         (Proofterm.proof_combt
-                          (PThm (corr_header, corr_body), vfs_of corr_prop),
+                          (PThm (corr_header, make_proof_body corr_prf), vfs_of corr_prop),
                             map PBound (length shyps - 1 downto 0)) |>
                       fold_rev Proofterm.forall_intr_proof'
                         (map (get_var_type corr_prop) (vfs_of prop)) |>
@@ -746,10 +760,9 @@
                       Proofterm.thm_header (serial ()) pos theory_name
                         (corr_name s vs') corr_prop
                         (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
-                    val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf');
                     val corr_prf'' =
                       Proofterm.proof_combP (Proofterm.proof_combt
-                        (PThm (corr_header, corr_body), vfs_of corr_prop),
+                        (PThm (corr_header, make_proof_body corr_prf), vfs_of corr_prop),
                              map PBound (length shyps - 1 downto 0)) |>
                       fold_rev Proofterm.forall_intr_proof'
                         (map (get_var_type corr_prop) (vfs_of prop)) |>
diff -r 35a4ef9c6d80 -r 00b67aaa4010 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Aug 20 11:38:48 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Aug 20 14:55:27 2019 +0200
@@ -45,6 +45,7 @@
   val thm_node_body: thm_node -> proof_body future
   val join_thms: pthm list -> proof_body list
   val consolidate: proof_body list -> unit
+  val make_thm: thm_header -> thm_body -> pthm
   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) ->
@@ -53,7 +54,6 @@
   val thm_ord: pthm ord
   val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
   val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T
-  val approximate_proof_body: proof -> proof_body
   val no_proof_body: proof -> proof_body
   val no_thm_proofs: proof -> proof
   val no_body_proofs: proof -> proof
@@ -249,6 +249,9 @@
         let val PBody {thms, ...} = Future.join body
         in consolidate (join_thms thms) end)};
 
+fun make_thm ({serial, name, prop, ...}: thm_header) (Thm_Body {body, ...}) =
+  (serial, make_thm_node name prop body);
+
 
 (* proof atoms *)
 
@@ -290,20 +293,6 @@
 val unions_oracles = Ord_List.unions oracle_ord;
 val unions_thms = Ord_List.unions thm_ord;
 
-fun approximate_proof_body prf =
-  let
-    val (oracles, thms) = fold_proof_atoms false
-      (fn Oracle (s, prop, _) => apfst (cons (s, prop))
-        | PThm ({serial = i, name, prop, ...}, Thm_Body {body, ...}) =>
-            apsnd (cons (i, make_thm_node name prop body))
-        | _ => I) [prf] ([], []);
-  in
-    PBody
-     {oracles = Ord_List.make oracle_ord oracles,
-      thms = Ord_List.make thm_ord thms,
-      proof = prf}
-  end;
-
 fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof};
 val no_thm_body = thm_body (no_proof_body MinProof);