src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/HOL.thy	Fri Dec 17 17:43:54 2010 +0100
@@ -103,9 +103,8 @@
 notation (xsymbols)
   iff  (infixr "\<longleftrightarrow>" 25)
 
-nonterminals
-  letbinds  letbind
-  case_syn  cases_syn
+nonterminal letbinds and letbind
+nonterminal case_syn and cases_syn
 
 syntax
   "_The"        :: "[pttrn, bool] => 'a"                 ("(3THE _./ _)" [0, 10] 10)