--- a/src/HOL/List.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/List.thy Fri Dec 17 17:43:54 2010 +0100
@@ -123,7 +123,7 @@
"list_update [] i v = []"
| "list_update (x # xs) i v = (case i of 0 \<Rightarrow> v # xs | Suc j \<Rightarrow> x # list_update xs j v)"
-nonterminals lupdbinds lupdbind
+nonterminal lupdbinds and lupdbind
syntax
"_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)")
@@ -346,7 +346,7 @@
@{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.
*)
-nonterminals lc_qual lc_quals
+nonterminal lc_qual and lc_quals
syntax
"_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ . __")