1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Apr 10 17:01:37 2008 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Apr 10 17:01:38 2008 +0200
     1.3 @@ -625,32 +625,32 @@
     1.4  val _ =
     1.5    OuterSyntax.command "qed" "conclude (sub-)proof"
     1.6      (K.tag_proof K.qed_block)
     1.7 -    (Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.qed));
     1.8 +    (Scan.option Method.parse >> (Toplevel.print oo IsarCmd.qed));
     1.9  
    1.10  val _ =
    1.11    OuterSyntax.command "by" "terminal backward proof"
    1.12      (K.tag_proof K.qed)
    1.13 -    (Method.parse -- Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.terminal_proof));
    1.14 +    (Method.parse -- Scan.option Method.parse >> (Toplevel.print oo IsarCmd.terminal_proof));
    1.15  
    1.16  val _ =
    1.17    OuterSyntax.command ".." "default proof"
    1.18      (K.tag_proof K.qed)
    1.19 -    (Scan.succeed (Toplevel.print3 o IsarCmd.default_proof));
    1.20 +    (Scan.succeed (Toplevel.print o IsarCmd.default_proof));
    1.21  
    1.22  val _ =
    1.23    OuterSyntax.command "." "immediate proof"
    1.24      (K.tag_proof K.qed)
    1.25 -    (Scan.succeed (Toplevel.print3 o IsarCmd.immediate_proof));
    1.26 +    (Scan.succeed (Toplevel.print o IsarCmd.immediate_proof));
    1.27  
    1.28  val _ =
    1.29    OuterSyntax.command "done" "done proof"
    1.30      (K.tag_proof K.qed)
    1.31 -    (Scan.succeed (Toplevel.print3 o IsarCmd.done_proof));
    1.32 +    (Scan.succeed (Toplevel.print o IsarCmd.done_proof));
    1.33  
    1.34  val _ =
    1.35    OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)"
    1.36      (K.tag_proof K.qed)
    1.37 -    (Scan.succeed (Toplevel.print3 o IsarCmd.skip_proof));
    1.38 +    (Scan.succeed (Toplevel.print o IsarCmd.skip_proof));
    1.39  
    1.40  val _ =
    1.41    OuterSyntax.command "oops" "forget proof"