# HG changeset patch
# User wenzelm
# Date 1207839698 -7200
# Node ID c348bbe7c87d5f7adbc7e2c93ce5d653b20dadd6
# Parent  f3535afb58e8f5124eef67a3fa967df3a934906c
eliminated unused Toplevel.print3/three_buffers;

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