# HG changeset patch
# User wenzelm
# Date 1184192130 -7200
# Node ID b094f9b7a52db5aee7a3989c221e31ae660c8b89
# Parent  ab2edd87b91252948449b0c7ee890e36c6920d9e
command 'declare': proper thy_decl;

diff -r ab2edd87b912 -r b094f9b7a52d src/Pure/Isar/isar_syn.ML
--- 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)])));