diff -r a44479bde681 -r 017e33849f4d Nominal/nominal_inductive.ML
--- a/Nominal/nominal_inductive.ML	Tue Mar 22 12:18:30 2016 +0000
+++ b/Nominal/nominal_inductive.ML	Thu Apr 19 13:57:17 2018 +0100
@@ -434,7 +434,7 @@
   val avoids_parser =
     Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" single_avoid_parser) []
 
-  val main_parser = Parse.xname -- avoids_parser
+  val main_parser = Parse.name -- avoids_parser
 in
   val _ =
     Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive}