--- a/src/ZF/func.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/ZF/func.thy Fri Dec 17 17:43:54 2010 +0100
@@ -445,8 +445,7 @@
update :: "[i,i,i] => i" where
"update(f,a,b) == lam x: cons(a, domain(f)). if(x=a, b, f`x)"
-nonterminals
- updbinds updbind
+nonterminal updbinds and updbind
syntax