src/Pure/Isar/isar_syn.ML
changeset 20305 16c8f44b1852
parent 19844 2c1fdc397ded
child 20365 5fad57dfd7c9
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Aug 02 22:26:58 2006 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 02 22:26:59 2006 +0200
     1.3 @@ -506,7 +506,7 @@
     1.4  val endP =
     1.5    OuterSyntax.command "}" "end explicit proof block"
     1.6      (K.tag_proof K.prf_close)
     1.7 -    (Scan.succeed (Toplevel.print o Toplevel.proofs Proof.end_block));
     1.8 +    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
     1.9  
    1.10  val nextP =
    1.11    OuterSyntax.command "next" "enter next proof block"