1.1 --- a/src/HOL/Tools/groebner.ML	Thu Aug 26 13:44:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/groebner.ML	Thu Aug 26 20:51:17 2010 +0200
     1.3 @@ -931,7 +931,7 @@
     1.4    | Const (@{const_name Ex}, _) $ _ => find_body bounds (dest_arg tm)
     1.5    | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
     1.6    | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
     1.7 -  | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
     1.8 +  | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
     1.9    | @{term "op ==>"} $_$_ => find_args bounds tm
    1.10    | Const("op ==",_)$_$_ => find_args bounds tm
    1.11    | @{term Trueprop}$_ => find_term bounds (dest_arg tm)