src/HOL/Fun.thy

--- a/src/HOL/Fun.thy	Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/Fun.thy	Fri Dec 17 17:43:54 2010 +0100
@@ -558,8 +558,8 @@
   fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where
   "fun_upd f a b == % x. if x=a then b else f x"
 
-nonterminals
-  updbinds updbind
+nonterminal updbinds and updbind
+
 syntax
   "_updbind" :: "['a, 'a] => updbind"             ("(2_ :=/ _)")
   ""         :: "updbind => updbinds"             ("_")