# HG changeset patch
# User wenzelm
# Date 934833828 -7200
# Node ID e4244b2e70ef05be6d7a47bf36c4a7fc6c5c8e61
# Parent  13e43b7456a1de6fa14ccbfcfa2f05fe59cea0b6
disable_pr, enable_pr;

diff -r 13e43b7456a1 -r e4244b2e70ef src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Aug 16 18:47:20 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Aug 16 22:03:48 1999 +0200
@@ -527,10 +527,14 @@
   OuterSyntax.improper_command "pr" "print current toplevel state" K.diag
     (Scan.succeed (Toplevel.print o Toplevel.imperative (fn () => Toplevel.quiet := false)));
 
-val no_prP =
-  OuterSyntax.improper_command "no_pr" "disable printing of toplevel state" K.diag
+val disable_prP =
+  OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag
     (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := true)));
 
+val enable_prP =
+  OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag
+    (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := false)));
+
 
 val opt_unit = Scan.optional (P.$$$ "(" -- P.$$$ ")" >> (K ())) ();
 
@@ -588,8 +592,8 @@
   print_lthmsP, print_thmsP, 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, remove_thyP, prP, no_prP, commitP,
-  quitP, exitP, init_toplevelP];
+  touch_thyP, touch_all_thysP, remove_thyP, prP, disable_prP,
+  enable_prP, commitP, quitP, exitP, init_toplevelP];
 
 
 end;