# HG changeset patch
# User oheimb
# Date 902928134 -7200
# Node ID 25fb5156e0d987bd5c1e1250e5fb475c7c8e929a
# Parent  a84dd70e992577d935ea1b7204a7891add1b326a
replaced idt by pttrn in @filter

diff -r a84dd70e9925 -r 25fb5156e0d9 src/HOL/List.thy
--- 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