# HG changeset patch
# User wenzelm
# Date 1470500099 -7200
# Node ID 994d1a1105ef1679d6352c2a52d17511ee00d81e
# Parent  1a38142e11727382250d5842b95bd955a8b4bec2
more informative 'prf' and 'full_prf', based on HOL/Proofs/ex/XML_Data.thy;

diff -r 1a38142e1172 -r 994d1a1105ef NEWS
--- a/NEWS	Sat Aug 06 17:39:21 2016 +0200
+++ b/NEWS	Sat Aug 06 18:14:59 2016 +0200
@@ -57,6 +57,9 @@
 theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order
 is relevant to avoid confusion of Pure.simp vs. HOL.simp.
 
+* Commands 'prf' and 'full_prf' are somewhat more informative (again):
+proof terms are reconstructed and cleaned from administrative thm nodes.
+
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
diff -r 1a38142e1172 -r 994d1a1105ef src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Aug 06 17:39:21 2016 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Aug 06 18:14:59 2016 +0200
@@ -84,10 +84,8 @@
     \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> do not have any permanent effect.
 
     \<^descr> @{command "prf"} displays the (compact) proof term of the current proof
-    state (if present), or of the given theorems. Note that this requires
-    proof terms to be switched on for the current object logic (see the
-    ``Proof terms'' section of the Isabelle reference manual for information
-    on how to do this).
+    state (if present), or of the given theorems. Note that this requires an
+    underlying logic image with proof terms enabled, e.g. \<open>HOL-Proofs\<close>.
 
     \<^descr> @{command "full_prf"} is like @{command "prf"}, but displays the full
     proof term, i.e.\ also displays information omitted in the compact proof
diff -r 1a38142e1172 -r 994d1a1105ef src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Aug 06 17:39:21 2016 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Aug 06 18:14:59 2016 +0200
@@ -258,9 +258,24 @@
             (if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf')
         end
     | SOME srcs =>
-        let val ctxt = Toplevel.context_of state
-        in map (Proof_Syntax.pretty_proof_of ctxt full) (Attrib.eval_thms ctxt srcs) end
-        |> Pretty.chunks);
+        let
+          val ctxt = Toplevel.context_of state;
+          val thy = Proof_Context.theory_of ctxt;
+          fun pretty_proof thm =
+            let
+              val (_, prop) =
+                Logic.unconstrainT (Thm.shyps_of thm)
+                  (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
+            in
+              Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
+              |> Reconstruct.reconstruct_proof ctxt prop
+              |> Reconstruct.expand_proof ctxt [("", NONE)]
+              |> Proofterm.rew_proof thy
+              |> Proofterm.no_thm_proofs
+              |> not full ? Proofterm.shrink_proof
+              |> Proof_Syntax.pretty_proof ctxt
+            end;
+        in Pretty.chunks (map pretty_proof (Attrib.eval_thms ctxt srcs)) end);
 
 fun string_of_prop ctxt s =
   let