--- 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))));