diff -r e1fce873b814 -r d797baa3d57c src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Fri Dec 17 17:08:56 2010 +0100
+++ b/src/ZF/ZF.thy	Fri Dec 17 17:43:54 2010 +0100
@@ -102,7 +102,7 @@
   where "A -> B == Pi(A, %_. B)"
 
 
-nonterminals "is" patterns
+nonterminal "is" and patterns
 
 syntax
   ""          :: "i => is"                   ("_")