# HG changeset patch
# User wenzelm
# Date 1028317228 -7200
# Node ID 063c2190812b5c7c35491b38b6bd0528141731d1
# Parent  4cfead92f8f7d9ad33bf9200477192962ca1f056
fixed long statement: P.opt_thm_name;

diff -r 4cfead92f8f7 -r 063c2190812b src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Aug 02 17:52:51 2002 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Aug 02 21:40:28 2002 +0200
@@ -304,7 +304,7 @@
 
 fun gen_theorem k =
   OuterSyntax.command k ("state " ^ k) K.thy_goal
-    (P.locale_target -- Scan.optional (P.thm_name ":" --|
+    (P.locale_target -- Scan.optional (P.opt_thm_name ":" --|
       Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
       general_statement >> (fn ((x, y), (z, w)) =>
       (Toplevel.print o Toplevel.theory_to_proof (IsarThy.smart_multi_theorem k x y z w))));