Added functions for printing primitive proof terms.

--- a/src/Pure/Isar/isar_cmd.ML	Fri Aug 31 16:17:52 2001 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Aug 31 16:20:19 2001 +0200
@@ -57,6 +57,8 @@
   val print_cases: Toplevel.transition -> Toplevel.transition
   val print_thms: (string list * (string * Args.src list) list) * Comment.text
     -> Toplevel.transition -> Toplevel.transition
+  val print_prfs: bool -> (string list * (string * Args.src list) list) * Comment.text
+    -> Toplevel.transition -> Toplevel.transition
   val print_prop: (string list * string) * Comment.text
     -> Toplevel.transition -> Toplevel.transition
   val print_term: (string list * string) * Comment.text
@@ -223,6 +225,10 @@
 fun string_of_thms state ms args = with_modes ms (fn () =>
   Pretty.string_of (Proof.pretty_thms (IsarThy.get_thmss args state)));
 
+fun string_of_prfs full state ms args = with_modes ms (fn () =>
+  Pretty.string_of (Pretty.chunks
+    (map (ProofSyntax.pretty_proof_of full) (IsarThy.get_thmss args state))));
+
 fun string_of_prop state ms s =
   let
     val sign = Proof.sign_of state;
@@ -250,6 +256,7 @@
   writeln (string_of (Toplevel.enter_forward_proof state) x y));
 
 val print_thms = print_item string_of_thms o Comment.ignore;
+fun print_prfs full = print_item (string_of_prfs full) o Comment.ignore;
 val print_prop = print_item string_of_prop o Comment.ignore;
 val print_term = print_item string_of_term o Comment.ignore;
 val print_type = print_item string_of_type o Comment.ignore;

--- a/src/Pure/Isar/isar_output.ML	Fri Aug 31 16:17:52 2001 +0200
+++ b/src/Pure/Isar/isar_output.ML	Fri Aug 31 16:20:19 2001 +0200
@@ -296,6 +296,9 @@
 fun pretty_thm ctxt thms =
   Pretty.chunks (map (pretty_term ctxt o #prop o Thm.rep_thm) thms);
 
+fun pretty_prf full ctxt thms =
+  Pretty.chunks (map (ProofSyntax.pretty_proof_of full) thms);
+
 fun output_with pretty src ctxt x =
   let
     val prt = pretty ctxt x;      (*always pretty!*)
@@ -311,6 +314,8 @@
 val _ = add_commands
  [("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
   ("thm", args Attrib.local_thmss (output_with pretty_thm)),
+  ("prf", args Attrib.local_thmss (output_with (pretty_prf false))),
+  ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true))),
   ("prop", args Args.local_prop (output_with pretty_term)),
   ("term", args Args.local_term (output_with pretty_term)),
   ("typ", args Args.local_typ_no_norm (output_with pretty_typ)),

--- a/src/Pure/Isar/isar_syn.ML	Fri Aug 31 16:17:52 2001 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Aug 31 16:20:19 2001 +0200
@@ -563,6 +563,14 @@
   OuterSyntax.improper_command "thm" "print theorems" K.diag
     (opt_modes -- P.xthms1 -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_thms));
 
+val print_prfsP =
+  OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag
+    (opt_modes -- P.xthms1 -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
+
+val print_full_prfsP =
+  OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag
+    (opt_modes -- P.xthms1 -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
+
 val print_propP =
   OuterSyntax.improper_command "prop" "read and print proposition" K.diag
     (opt_modes -- P.term -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_prop));
@@ -698,7 +706,8 @@
   print_syntaxP, print_theoremsP, print_attributesP,
   print_trans_rulesP, print_methodsP, print_antiquotationsP,
   thms_containingP, thm_depsP, print_bindsP, print_lthmsP,
-  print_casesP, print_thmsP, print_propP, print_termP, print_typeP,
+  print_casesP, print_thmsP, print_prfsP, print_full_prfsP,
+  print_propP, print_termP, print_typeP,
   (*system commands*)
   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,