# HG changeset patch
# User wenzelm
# Date 1414663706 -3600
# Node ID aa8cf5eed06ed85eb2ca2b07bc0686fa19802997
# Parent  e05c620eceebb58f650edcb6354c2f5b653d92c7
proper syntax categery "name" -- as usual and as documented;

diff -r e05c620eceeb -r aa8cf5eed06e src/HOL/Library/bnf_axiomatization.ML
--- a/src/HOL/Library/bnf_axiomatization.ML	Thu Oct 30 09:15:54 2014 +0100
+++ b/src/HOL/Library/bnf_axiomatization.ML	Thu Oct 30 11:08:26 2014 +0100
@@ -105,7 +105,7 @@
 val bnf_axiomatization_cmd = prepare_decl Plugin_Name.make_filter read_constraint Syntax.read_typ;
 
 val parse_witTs =
-  @{keyword "["} |-- (Parse.short_ident --| @{keyword ":"} -- Scan.repeat Parse.typ
+  @{keyword "["} |-- (Parse.name --| @{keyword ":"} -- Scan.repeat Parse.typ
     >> (fn ("wits", Ts) => Ts
          | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --|
   @{keyword "]"} || Scan.succeed [];
diff -r e05c620eceeb -r aa8cf5eed06e src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Thu Oct 30 09:15:54 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Thu Oct 30 11:08:26 2014 +0100
@@ -127,7 +127,7 @@
   @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
   Scan.succeed [];
 
-val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- Parse.binding;
+val parse_map_rel_binding = Parse.name --| @{keyword ":"} -- Parse.binding;
 
 val no_map_rel = (Binding.empty, Binding.empty);
 
diff -r e05c620eceeb -r aa8cf5eed06e src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu Oct 30 09:15:54 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu Oct 30 11:08:26 2014 +0100
@@ -289,8 +289,7 @@
 
 val parse_metis_options =
   Scan.optional
-      (Args.parens (Parse.short_ident
-                    -- Scan.option (@{keyword ","} |-- Parse.short_ident))
+      (Args.parens (Args.name -- Scan.option (@{keyword ","} |-- Args.name))
        >> (fn (s, s') =>
               (NONE, NONE) |> consider_opt s
                            |> (case s' of SOME s' => consider_opt s' | _ => I)))
diff -r e05c620eceeb -r aa8cf5eed06e src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Oct 30 09:15:54 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Oct 30 11:08:26 2014 +0100
@@ -409,7 +409,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "sledgehammer"}
     "search for first-order proof using automatic theorem provers"
-    ((Scan.optional Parse.short_ident runN -- parse_params
+    ((Scan.optional Parse.name runN -- parse_params
       -- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
 val _ =
   Outer_Syntax.command @{command_spec "sledgehammer_params"}