20070619-2

It should be OK to use _ instead of the original pattern when defining a function using with. Example problem:

 module Bug where

 data Foo : Set where
   foo : Foo

 f : Foo -> Foo
 f foo with foo
 f _   | foo = foo

 Bug.agda:7,1-8,18
 With clause pattern _ is not an instance of its parent pattern
 when checking that the clause
 f foo with foo
 f _ | foo = foo
 has type Foo -> Foo

No it shouldn't.