src/HOL/Record.thy
changeset 41229 d797baa3d57c
parent 38539 3be65f879bcd
child 42695 a94ad372b2f5
--- a/src/HOL/Record.thy	Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/Record.thy	Fri Dec 17 17:43:54 2010 +0100
@@ -419,8 +419,15 @@
 
 subsection {* Concrete record syntax *}
 
-nonterminals
-  ident field_type field_types field fields field_update field_updates
+nonterminal
+  ident and
+  field_type and
+  field_types and
+  field and
+  fields and
+  field_update and
+  field_updates
+
 syntax
   "_constify"           :: "id => ident"                        ("_")
   "_constify"           :: "longid => ident"                    ("_")