--- 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 ***
--- 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
--- 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