# HG changeset patch
# User wenzelm
# Date 1573236410 -3600
# Node ID 4b45d592ce290f7ec415792afd9a06398c866e3b
# Parent  77580c977e0ca2370207e8ecade9368ab1c6be51
clarified modules;

diff -r 77580c977e0c -r 4b45d592ce29 src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Fri Nov 08 16:25:18 2019 +0100
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Fri Nov 08 19:06:50 2019 +0100
@@ -13,7 +13,7 @@
 
 ML \<open>
   fun export_proof thy thm = thm
-    |> Thm.standard_proof_of {full = true, expand_name = Thm.expand_name thm}
+    |> Proof_Syntax.standard_proof_of {full = true, expand_name = Thm.expand_name thm}
     |> Proofterm.encode (Sign.consts_of thy);
 
   fun import_proof thy xml =
diff -r 77580c977e0c -r 4b45d592ce29 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Fri Nov 08 16:25:18 2019 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Nov 08 19:06:50 2019 +0100
@@ -14,9 +14,11 @@
   val proof_syntax: Proofterm.proof -> theory -> theory
   val proof_of: bool -> thm -> Proofterm.proof
   val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
-  val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
   val pretty_proof_boxes_of: Proof.context ->
     {full: bool, preproc: theory -> proof -> proof} -> thm -> Pretty.T
+  val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> string option} ->
+    thm -> Proofterm.proof
+  val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
 end;
 
 structure Proof_Syntax : PROOF_SYNTAX =
@@ -251,9 +253,6 @@
     (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
     (term_of_proof prf);
 
-fun pretty_standard_proof_of ctxt full thm =
-  pretty_proof ctxt (Thm.standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm);
-
 fun pretty_proof_boxes_of ctxt {full, preproc} thm =
   let
     val thy = Proof_Context.theory_of ctxt;
@@ -280,4 +279,19 @@
     |> Pretty.chunks
   end;
 
+
+(* standardized proofs *)
+
+fun standard_proof_of {full, expand_name} thm =
+  let val thy = Thm.theory_of_thm thm in
+    Thm.reconstruct_proof_of thm
+    |> Proofterm.expand_proof thy expand_name
+    |> Proofterm.rew_proof thy
+    |> Proofterm.no_thm_proofs
+    |> not full ? Proofterm.shrink_proof
+  end;
+
+fun pretty_standard_proof_of ctxt full thm =
+  pretty_proof ctxt (standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm);
+
 end;
diff -r 77580c977e0c -r 4b45d592ce29 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Nov 08 16:25:18 2019 +0100
+++ b/src/Pure/ROOT.ML	Fri Nov 08 19:06:50 2019 +0100
@@ -287,8 +287,8 @@
 ML_file "Isar/toplevel.ML";
 
 (*proof term operations*)
+ML_file "Proof/proof_rewrite_rules.ML";
 ML_file "Proof/proof_syntax.ML";
-ML_file "Proof/proof_rewrite_rules.ML";
 ML_file "Proof/proof_checker.ML";
 ML_file "Proof/extraction.ML";
 
diff -r 77580c977e0c -r 4b45d592ce29 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Fri Nov 08 16:25:18 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Fri Nov 08 19:06:50 2019 +0100
@@ -270,7 +270,8 @@
 
         val proof0 =
           if Proofterm.export_standard_enabled () then
-            Thm.standard_proof_of {full = true, expand_name = SOME o expand_name thm_id} thm
+            Proof_Syntax.standard_proof_of
+              {full = true, expand_name = SOME o expand_name thm_id} thm
           else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm
           else MinProof;
         val (prop, SOME proof) =
diff -r 77580c977e0c -r 4b45d592ce29 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Fri Nov 08 16:25:18 2019 +0100
+++ b/src/Pure/more_thm.ML	Fri Nov 08 19:06:50 2019 +0100
@@ -113,9 +113,6 @@
   val tag: string * string -> attribute
   val untag: string -> attribute
   val kind: string -> attribute
-  val reconstruct_proof_of: thm -> Proofterm.proof
-  val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> string option} ->
-    thm -> Proofterm.proof
   val register_proofs: thm list lazy -> theory -> theory
   val consolidate_theory: theory -> unit
   val expose_theory: theory -> unit
@@ -653,22 +650,6 @@
 
 
 
-(** proof terms **)
-
-fun reconstruct_proof_of thm =
-  Proofterm.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
-
-fun standard_proof_of {full, expand_name} thm =
-  let val thy = Thm.theory_of_thm thm in
-    reconstruct_proof_of thm
-    |> Proofterm.expand_proof thy expand_name
-    |> Proofterm.rew_proof thy
-    |> Proofterm.no_thm_proofs
-    |> not full ? Proofterm.shrink_proof
-  end;
-
-
-
 (** forked proofs **)
 
 structure Proofs = Theory_Data
diff -r 77580c977e0c -r 4b45d592ce29 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Nov 08 16:25:18 2019 +0100
+++ b/src/Pure/thm.ML	Fri Nov 08 19:06:50 2019 +0100
@@ -101,6 +101,7 @@
   val proof_bodies_of: thm list -> proof_body list
   val proof_body_of: thm -> proof_body
   val proof_of: thm -> proof
+  val reconstruct_proof_of: thm -> Proofterm.proof
   val consolidate: thm list -> unit
   val expose_proofs: theory -> thm list -> unit
   val expose_proof: theory -> thm -> unit
@@ -760,6 +761,9 @@
 val proof_body_of = singleton proof_bodies_of;
 val proof_of = Proofterm.proof_of o proof_body_of;
 
+fun reconstruct_proof_of thm =
+  Proofterm.reconstruct_proof (theory_of_thm thm) (prop_of thm) (proof_of thm);
+
 val consolidate = ignore o proof_bodies_of;
 
 fun expose_proofs thy thms =