1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Mar 01 17:07:36 2010 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Mar 01 17:09:42 2010 +0100
     1.3 @@ -226,6 +226,16 @@
     1.4      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
     1.5  
     1.6  val _ =
     1.7 +  OuterSyntax.local_theory "type_notation" "add notation for type constructors" K.thy_decl
     1.8 +    (opt_mode -- P.and_list1 (P.xname -- P.mixfix)
     1.9 +    >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
    1.10 +
    1.11 +val _ =
    1.12 +  OuterSyntax.local_theory "no_type_notation" "delete notation for type constructors" K.thy_decl
    1.13 +    (opt_mode -- P.and_list1 (P.xname -- P.mixfix)
    1.14 +    >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
    1.15 +
    1.16 +val _ =
    1.17    OuterSyntax.local_theory "notation" "add notation for constants / fixed variables" K.thy_decl
    1.18      (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
    1.19      >> (fn (mode, args) => Specification.notation_cmd true mode args));