fixed long statement: P.opt_thm_name;
authorwenzelm
Fri, 02 Aug 2002 21:40:28 +0200
changeset 13445 063c2190812b
parent 13444 4cfead92f8f7
child 13446 f0fdd0499dad
fixed long statement: P.opt_thm_name;
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))));