src/Pure/Isar/isar_syn.ML

   OuterSyntax.command "lemmas" "define lemmas" K.thy_decl
     (theorems Drule.lemmaK >> Toplevel.theory);
 
 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));
 
 
 (* name space entry path *)