src/Pure/Isar/isar_syn.ML
changeset 6530 473305b71b74
parent 6512 d174c937bf93
child 6551 de4047b03017
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Apr 27 15:13:35 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 27 15:13:58 1999 +0200
     1.3 @@ -323,15 +323,15 @@
     1.4  
     1.5  val terminal_proofP =
     1.6    OuterSyntax.command "by" "terminal backward proof"
     1.7 -    (method >> (Toplevel.print oo IsarThy.terminal_proof));
     1.8 +    (method >> IsarThy.terminal_proof)
     1.9  
    1.10  val immediate_proofP =
    1.11    OuterSyntax.command "." "immediate proof"
    1.12 -    (Scan.succeed (Toplevel.print o IsarThy.immediate_proof));
    1.13 +    (Scan.succeed IsarThy.immediate_proof);
    1.14  
    1.15  val default_proofP =
    1.16    OuterSyntax.command ".." "default proof"
    1.17 -    (Scan.succeed (Toplevel.print o IsarThy.default_proof));
    1.18 +    (Scan.succeed IsarThy.default_proof);
    1.19  
    1.20  
    1.21  (* proof steps *)