| changeset 15570 | 8d8c70b41bab |
| parent 15531 | 08c8dad8e399 |
| child 15596 | 8665d08085df |
--- 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));