src/Pure/Isar/isar_syn.ML
changeset 21403 dd58f13a8eb4
parent 21350 6e58289b6685
child 21437 a3c55b85cf0e
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Nov 17 02:19:54 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Nov 17 02:19:55 2006 +0100
     1.3 @@ -218,7 +218,7 @@
     1.4  
     1.5  val notationP =
     1.6    OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl
     1.7 -    (P.opt_locale_target -- opt_mode -- Scan.repeat1 (P.xname -- P.mixfix)
     1.8 +    (P.opt_locale_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
     1.9      >> (fn ((loc, mode), args) =>
    1.10          Toplevel.local_theory loc (Specification.notation mode args)));
    1.11