--- 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 =
--- 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;
--- 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";
--- 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) =
--- 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
--- 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 =