# HG changeset patch
# User wenzelm
# Date 1192828871 -7200
# Node ID ca5708210cb8c1ab018a6454a065e566d55060e4
# Parent  dbf09ca6a80e254d2108d3d57929e89b5f359e64
sorry: proper command;

diff -r dbf09ca6a80e -r ca5708210cb8 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Oct 19 23:21:08 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Oct 19 23:21:11 2007 +0200
@@ -641,7 +641,7 @@
     (Scan.succeed (Toplevel.print3 o IsarCmd.done_proof));
 
 val _ =
-  OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)"
+  OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)"
     (K.tag_proof K.qed)
     (Scan.succeed (Toplevel.print3 o IsarCmd.skip_proof));