src/HOL/HOLCF/ex/Letrec.thy

--- a/src/HOL/HOLCF/ex/Letrec.thy	Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/HOLCF/ex/Letrec.thy	Fri Dec 17 17:43:54 2010 +0100
@@ -14,8 +14,7 @@
   CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
   "CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))"
 
-nonterminals
-  recbinds recbindt recbind
+nonterminal recbinds and recbindt and recbind
 
 syntax
   "_recbind"  :: "['a, 'a] \<Rightarrow> recbind"               ("(2_ =/ _)" 10)