diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -117,7 +117,7 @@
     "associate SPARK types with types"
     (Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ --
        Scan.optional (Args.parens (Parse.list1
-         (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.xname)))) [])) >>
+         (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.name)))) [])) >>
        (Toplevel.theory o fold add_spark_type_cmd));
 
 val _ =