--- a/src/HOL/List.thy Mon May 13 15:27:28 2002 +0200
+++ b/src/HOL/List.thy Mon May 13 15:39:56 2002 +0200
@@ -41,8 +41,7 @@
"distinct":: "'a list => bool"
replicate :: "nat => 'a => 'a list"
-nonterminals
-lupdbindslupdbind
+nonterminals lupdbinds lupdbind
syntax
-- {* list Enumeration *}