diff -r 1b3115d1a8df -r 8d8c70b41bab src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Mar 03 09:22:35 2005 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 03 12:43:01 2005 +0100
@@ -214,7 +214,7 @@
 
 val declareP =
   OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
-    (P.locale_target -- (P.and_list1 P.xthms1 >> flat)
+    (P.locale_target -- (P.and_list1 P.xthms1 >> List.concat)
       >> (Toplevel.theory o uncurry IsarThy.declare_theorems));