src/Pure/Isar/isar_syn.ML
changeset 24953 f92386569176
parent 24950 106fc30769a9
child 24960 39d1dd215d73
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Oct 10 17:32:00 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 11 00:28:30 2007 +0200
     1.3 @@ -244,13 +244,13 @@
     1.4  
     1.5  val _ =
     1.6    OuterSyntax.command "notation" "add notation for constants / fixed variables" K.thy_decl
     1.7 -    (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
     1.8 +    (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
     1.9      >> (fn ((loc, mode), args) =>
    1.10          Toplevel.local_theory loc (Specification.notation_cmd true mode args)));
    1.11  
    1.12  val _ =
    1.13    OuterSyntax.command "no_notation" "delete notation for constants / fixed variables" K.thy_decl
    1.14 -    (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
    1.15 +    (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
    1.16      >> (fn ((loc, mode), args) =>
    1.17          Toplevel.local_theory loc (Specification.notation_cmd false mode args)));
    1.18