command 'declare': proper thy_decl;

--- a/src/Pure/Isar/isar_syn.ML	Thu Jul 12 00:15:28 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 12 00:15:30 2007 +0200
@@ -255,7 +255,7 @@
   OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
 
 val declareP =
-  OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
+  OuterSyntax.command "declare" "declare theorems (improper)" K.thy_decl
     (P.opt_target -- (P.and_list1 SpecParse.xthms1 >> flat)
       >> (fn (loc, args) => Toplevel.local_theory loc
           (#2 o Specification.theorems "" [(("", []), args)])));