# HG changeset patch
# User wenzelm
# Date 1570823470 -7200
# Node ID 2136e4670ad2e81e9a22ea1239214eb1935bb48e
# Parent  e381e2624077c62f2f8a580e4b9b2aa34ea30ec7
clarified standard_proof_of: prefer expand_proof over somewhat adhoc strip_thm_proof;

diff -r e381e2624077 -r 2136e4670ad2 src/HOL/Proofs/ex/Proof_Terms.thy
--- a/src/HOL/Proofs/ex/Proof_Terms.thy	Fri Oct 11 21:44:39 2019 +0200
+++ b/src/HOL/Proofs/ex/Proof_Terms.thy	Fri Oct 11 21:51:10 2019 +0200
@@ -29,8 +29,8 @@
   val prf = Proofterm.proof_of body;
 
   (*clean output*)
-  Pretty.writeln (Proof_Syntax.pretty_clean_proof_of \<^context> false thm);
-  Pretty.writeln (Proof_Syntax.pretty_clean_proof_of \<^context> true thm);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);
 
   (*all theorems used in the graph of nested proofs*)
   val all_thms =
diff -r e381e2624077 -r 2136e4670ad2 src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Fri Oct 11 21:44:39 2019 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Fri Oct 11 21:51:10 2019 +0200
@@ -13,7 +13,8 @@
 
 ML \<open>
   fun export_proof thy thm =
-    Proofterm.encode (Sign.consts_of thy) (Thm.clean_proof_of true thm);
+    Proofterm.encode (Sign.consts_of thy)
+      (Proofterm.reconstruct_proof thy (Thm.prop_of thm) (Thm.standard_proof_of true thm));
 
   fun import_proof thy xml =
     let
diff -r e381e2624077 -r 2136e4670ad2 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Oct 11 21:44:39 2019 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Oct 11 21:51:10 2019 +0200
@@ -250,7 +250,7 @@
     | SOME srcs =>
         let
           val ctxt = Toplevel.context_of state;
-          val pretty_proof = Proof_Syntax.pretty_clean_proof_of ctxt full;
+          val pretty_proof = Proof_Syntax.pretty_standard_proof_of ctxt full;
         in Pretty.chunks (map pretty_proof (Attrib.eval_thms ctxt srcs)) end);
 
 fun string_of_prop ctxt s =
diff -r e381e2624077 -r 2136e4670ad2 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Fri Oct 11 21:44:39 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Oct 11 21:51:10 2019 +0200
@@ -13,7 +13,7 @@
   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_clean_proof_of: Proof.context -> bool -> thm -> Pretty.T
+  val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
 end;
 
 structure Proof_Syntax : PROOF_SYNTAX =
@@ -195,7 +195,7 @@
     (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
     (Proofterm.term_of_proof prf);
 
-fun pretty_clean_proof_of ctxt full thm =
-  pretty_proof ctxt (Thm.clean_proof_of full thm);
+fun pretty_standard_proof_of ctxt full thm =
+  pretty_proof ctxt (Thm.standard_proof_of full thm);
 
 end;
diff -r e381e2624077 -r 2136e4670ad2 src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Fri Oct 11 21:44:39 2019 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML	Fri Oct 11 21:51:10 2019 +0200
@@ -57,7 +57,7 @@
   let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s
   in Pretty.str (Proof_Context.extern_type ctxt name) end;
 
-fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full;
+fun pretty_prf full ctxt = Proof_Syntax.pretty_standard_proof_of ctxt full;
 
 fun pretty_theory ctxt (name, pos) =
   (Theory.check {long = true} ctxt (name, pos); Pretty.str name);
diff -r e381e2624077 -r 2136e4670ad2 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Fri Oct 11 21:44:39 2019 +0200
+++ b/src/Pure/more_thm.ML	Fri Oct 11 21:51:10 2019 +0200
@@ -114,7 +114,7 @@
   val untag: string -> attribute
   val kind: string -> attribute
   val reconstruct_proof_of: thm -> Proofterm.proof
-  val clean_proof_of: bool -> thm -> Proofterm.proof
+  val standard_proof_of: bool -> thm -> Proofterm.proof
   val register_proofs: thm list lazy -> theory -> theory
   val consolidate_theory: theory -> unit
   val show_consts: bool Config.T
@@ -656,16 +656,10 @@
 fun reconstruct_proof_of thm =
   Proofterm.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
 
-fun clean_proof_of full thm =
-  let
-    val thy = Thm.theory_of_thm thm;
-    val (_, prop) =
-      Logic.unconstrainT (Thm.shyps_of thm)
-        (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
-  in
-    Proofterm.strip_thm_proof (Thm.proof_of thm)
-    |> Proofterm.reconstruct_proof thy prop
-    |> Proofterm.expand_proof thy [("", NONE)]
+fun standard_proof_of full thm =
+  let val thy = Thm.theory_of_thm thm in
+    reconstruct_proof_of thm
+    |> Proofterm.expand_proof thy [("", NONE), (Thm.raw_derivation_name thm, NONE)]
     |> Proofterm.rew_proof thy
     |> Proofterm.no_thm_proofs
     |> not full ? Proofterm.shrink_proof
diff -r e381e2624077 -r 2136e4670ad2 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Oct 11 21:44:39 2019 +0200
+++ b/src/Pure/proofterm.ML	Fri Oct 11 21:51:10 2019 +0200
@@ -77,7 +77,6 @@
   val proof_combP: proof * proof list -> proof
   val strip_combt: proof -> proof * term option list
   val strip_combP: proof -> proof * proof list
-  val strip_thm_proof: proof -> proof
   val strip_thm_body: proof_body -> proof_body
   val map_proof_same: term Same.operation -> typ Same.operation
     -> (typ * class -> proof) -> proof Same.operation
@@ -450,11 +449,6 @@
           | stripc  x =  x
     in  stripc (prf, [])  end;
 
-fun strip_thm_proof proof =
-  (case fst (strip_combt (fst (strip_combP proof))) of
-    PThm (_, thm_body) => thm_body_proof_raw thm_body
-  | _ => proof);
-
 fun strip_thm_body (body as PBody {proof, ...}) =
   (case fst (strip_combt (fst (strip_combP proof))) of
     PThm (_, Thm_Body {body = body', ...}) => Future.join body'