src/HOL/Tools/groebner.ML
changeset 38786 e46e7a9cb622
parent 38558 32ad17fe2b9c
child 38795 848be46708dc
--- a/src/HOL/Tools/groebner.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/groebner.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -931,7 +931,7 @@
   | Const (@{const_name Ex}, _) $ _ => find_body bounds (dest_arg tm)
   | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
   | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
-  | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
+  | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
   | @{term "op ==>"} $_$_ => find_args bounds tm
   | Const("op ==",_)$_$_ => find_args bounds tm
   | @{term Trueprop}$_ => find_term bounds (dest_arg tm)