# HG changeset patch
# User wenzelm
# Date 925218838 -7200
# Node ID 473305b71b741396b573b7149d0e025c403ac125
# Parent  0f4c2ebc5018ccd3a730be5cd0fb6474b8af552f
no Toplevel.print for by, ., ..;

diff -r 0f4c2ebc5018 -r 473305b71b74 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Apr 27 15:13:35 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 27 15:13:58 1999 +0200
@@ -323,15 +323,15 @@
 
 val terminal_proofP =
   OuterSyntax.command "by" "terminal backward proof"
-    (method >> (Toplevel.print oo IsarThy.terminal_proof));
+    (method >> IsarThy.terminal_proof)
 
 val immediate_proofP =
   OuterSyntax.command "." "immediate proof"
-    (Scan.succeed (Toplevel.print o IsarThy.immediate_proof));
+    (Scan.succeed IsarThy.immediate_proof);
 
 val default_proofP =
   OuterSyntax.command ".." "default proof"
-    (Scan.succeed (Toplevel.print o IsarThy.default_proof));
+    (Scan.succeed IsarThy.default_proof);
 
 
 (* proof steps *)