# HG changeset patch
# User wenzelm
# Date 1302296392 -7200
# Node ID 0d1cbc1fe5790f2818acafc82353c3e6aa23828e
# Parent  06e93f257d0e99038413e85e0b440be420b7aa31
notation: proper markup for type constructor / constant;

diff -r 06e93f257d0e -r 0d1cbc1fe579 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Apr 08 22:50:50 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 08 22:59:52 2011 +0200
@@ -227,25 +227,25 @@
 val _ =
   Outer_Syntax.local_theory "type_notation" "add concrete syntax for type constructors"
     Keyword.thy_decl
-    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse.mixfix)
+    (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
       >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
 
 val _ =
   Outer_Syntax.local_theory "no_type_notation" "delete concrete syntax for type constructors"
     Keyword.thy_decl
-    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse.mixfix)
+    (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
       >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
 
 val _ =
   Outer_Syntax.local_theory "notation" "add concrete syntax for constants / fixed variables"
     Keyword.thy_decl
-    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
+    (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
       >> (fn (mode, args) => Specification.notation_cmd true mode args));
 
 val _ =
   Outer_Syntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables"
     Keyword.thy_decl
-    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
+    (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
       >> (fn (mode, args) => Specification.notation_cmd false mode args));
 
 
@@ -626,7 +626,7 @@
 val _ =
   Outer_Syntax.command "write" "add concrete syntax for constants / fixed variables"
     (Keyword.tag_proof Keyword.prf_decl)
-    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
+    (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
     >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
 
 val case_spec =
diff -r 06e93f257d0e -r 0d1cbc1fe579 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Fri Apr 08 22:50:50 2011 +0200
+++ b/src/Pure/Isar/parse.ML	Fri Apr 08 22:59:52 2011 +0200
@@ -91,6 +91,8 @@
   val prop_group: string parser
   val term: string parser
   val prop: string parser
+  val type_const: string parser
+  val const: string parser
   val literal_fact: string parser
   val propp: (string * string list) parser
   val termp: (string * string list) parser
@@ -327,6 +329,9 @@
 val term = inner_syntax term_group;
 val prop = inner_syntax prop_group;
 
+val type_const = inner_syntax (group "type constructor" xname);
+val const = inner_syntax (group "constant" xname);
+
 val literal_fact = inner_syntax (group "literal fact" alt_string);