# HG changeset patch
# User wenzelm
# Date 1010621550 -3600
# Node ID f8dfc78458916d1b9013e903a0eaaa43be68bb4b
# Parent  37cb8f7308f6dfe6c0beb151fdfd655271a688ac
IsarThy.smart_multi_theorem;

diff -r 37cb8f7308f6 -r f8dfc7845891 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Jan 10 01:12:01 2002 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jan 10 01:12:30 2002 +0100
@@ -298,7 +298,7 @@
 (* statements *)
 
 val in_locale_elems =
-  Scan.option ((P.$$$ "(" -- P.$$$ "in") |-- P.!!! (P.xname -- P.opt_attribs --| P.$$$ ")")) --
+  Scan.option ((P.$$$ "(" -- P.$$$ "in") |-- P.!!! (P.xname --| P.$$$ ")")) --
   Scan.optional (P.$$$ "(" |-- Scan.repeat1 P.locale_element --| P.!!! (P.$$$ ")")) [];
 
 val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- P.marg_comment);
@@ -308,7 +308,7 @@
   OuterSyntax.command k ("state " ^ k) K.thy_goal
     (Scan.optional (P.thm_name ":" --| Scan.ahead (P.$$$ "(")) ("", [])
       -- in_locale_elems -- statement' >> (fn ((x, y), z) =>
-      (Toplevel.print o Toplevel.theory_to_proof (IsarThy.multi_theorem k x y z))));
+      (Toplevel.print o Toplevel.theory_to_proof (IsarThy.smart_multi_theorem k x y z))));
 
 val theoremP = gen_theorem Drule.theoremK;
 val lemmaP = gen_theorem Drule.lemmaK;