--- a/src/HOL/List.thy Wed Aug 12 15:18:34 1998 +0200
+++ b/src/HOL/List.thy Wed Aug 12 15:22:14 1998 +0200
@@ -40,7 +40,7 @@
"@list" :: args => 'a list ("[(_)]")
(* Special syntax for filter *)
- "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
+ "@filter" :: [pttrn, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
(* list update *)
"_lupdbind" :: ['a, 'a] => lupdbind ("(2_ :=/ _)")
@@ -57,7 +57,7 @@
"xs[i:=x]" == "list_update xs i x"
syntax (symbols)
- "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_\\<in>_ ./ _])")
+ "@filter" :: [pttrn, 'a list, bool] => 'a list ("(1[_\\<in>_ ./ _])")
consts