# HG changeset patch
# User nipkow
# Date 1021297196 -7200
# Node ID f43153b6336119a319a87836ebd9f053b813140f
# Parent  59bc43b51aa26616a18e4c6c4298172ac48e2cf2
*** empty log message ***

diff -r 59bc43b51aa2 -r f43153b63361 src/HOL/List.thy
--- 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 *}