src/HOL/SPARK/Manual/Reference.thy

--- a/src/HOL/SPARK/Manual/Reference.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/SPARK/Manual/Reference.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -51,7 +51,7 @@
 @{rail \<open>
   @'spark_types' ((name '=' type (mapping?))+)
   ;
-  mapping: '('((name '=' nameref)+',')')'
+  mapping: '('((name '=' name)+',')')'
 \<close>}
 Associates a \SPARK{} type with the given name with an Isabelle type. This command can
 only be used outside a verification environment. The given type must be either a record