--- 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 _ =