src/Pure/Isar/isar_syn.ML
changeset 25108 ca5708210cb8
parent 25003 0b067b2d1b88
child 25192 b568f8c5d5ca
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Oct 19 23:21:08 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Oct 19 23:21:11 2007 +0200
     1.3 @@ -641,7 +641,7 @@
     1.4      (Scan.succeed (Toplevel.print3 o IsarCmd.done_proof));
     1.5  
     1.6  val _ =
     1.7 -  OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)"
     1.8 +  OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)"
     1.9      (K.tag_proof K.qed)
    1.10      (Scan.succeed (Toplevel.print3 o IsarCmd.skip_proof));
    1.11