# HG changeset patch
# User wenzelm
# Date 1208290164 -7200
# Node ID fb8039e26c6a98289d132a18504178361a0b75ce
# Parent  fba93ce71435dadbeb36be6e4cbef44c4fee908d
proof endings: no Toplevel.print!

diff -r fba93ce71435 -r fb8039e26c6a src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Apr 15 22:09:23 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 15 22:09:24 2008 +0200
@@ -625,32 +625,32 @@
 val _ =
   OuterSyntax.command "qed" "conclude (sub-)proof"
     (K.tag_proof K.qed_block)
-    (Scan.option Method.parse >> (Toplevel.print oo IsarCmd.qed));
+    (Scan.option Method.parse >> IsarCmd.qed);
 
 val _ =
   OuterSyntax.command "by" "terminal backward proof"
     (K.tag_proof K.qed)
-    (Method.parse -- Scan.option Method.parse >> (Toplevel.print oo IsarCmd.terminal_proof));
+    (Method.parse -- Scan.option Method.parse >> IsarCmd.terminal_proof);
 
 val _ =
   OuterSyntax.command ".." "default proof"
     (K.tag_proof K.qed)
-    (Scan.succeed (Toplevel.print o IsarCmd.default_proof));
+    (Scan.succeed IsarCmd.default_proof);
 
 val _ =
   OuterSyntax.command "." "immediate proof"
     (K.tag_proof K.qed)
-    (Scan.succeed (Toplevel.print o IsarCmd.immediate_proof));
+    (Scan.succeed IsarCmd.immediate_proof);
 
 val _ =
   OuterSyntax.command "done" "done proof"
     (K.tag_proof K.qed)
-    (Scan.succeed (Toplevel.print o IsarCmd.done_proof));
+    (Scan.succeed IsarCmd.done_proof);
 
 val _ =
   OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)"
     (K.tag_proof K.qed)
-    (Scan.succeed (Toplevel.print o IsarCmd.skip_proof));
+    (Scan.succeed IsarCmd.skip_proof);
 
 val _ =
   OuterSyntax.command "oops" "forget proof"