1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Apr 08 22:50:50 2011 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 08 22:59:52 2011 +0200
     1.3 @@ -227,25 +227,25 @@
     1.4  val _ =
     1.5    Outer_Syntax.local_theory "type_notation" "add concrete syntax for type constructors"
     1.6      Keyword.thy_decl
     1.7 -    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse.mixfix)
     1.8 +    (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
     1.9        >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
    1.10  
    1.11  val _ =
    1.12    Outer_Syntax.local_theory "no_type_notation" "delete concrete syntax for type constructors"
    1.13      Keyword.thy_decl
    1.14 -    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse.mixfix)
    1.15 +    (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
    1.16        >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
    1.17  
    1.18  val _ =
    1.19    Outer_Syntax.local_theory "notation" "add concrete syntax for constants / fixed variables"
    1.20      Keyword.thy_decl
    1.21 -    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
    1.22 +    (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
    1.23        >> (fn (mode, args) => Specification.notation_cmd true mode args));
    1.24  
    1.25  val _ =
    1.26    Outer_Syntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables"
    1.27      Keyword.thy_decl
    1.28 -    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
    1.29 +    (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
    1.30        >> (fn (mode, args) => Specification.notation_cmd false mode args));
    1.31  
    1.32  
    1.33 @@ -626,7 +626,7 @@
    1.34  val _ =
    1.35    Outer_Syntax.command "write" "add concrete syntax for constants / fixed variables"
    1.36      (Keyword.tag_proof Keyword.prf_decl)
    1.37 -    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
    1.38 +    (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
    1.39      >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
    1.40  
    1.41  val case_spec =