# HG changeset patch
# User nipkow
# Date 1513793857 -3600
# Node ID b2800da9eb8ad129c1a992da417cd9567572312e
# Parent  4ecf0ef70efb3e8bfa1f1ece38ddfc2bb3bb72c3
tuned op's

diff -r 4ecf0ef70efb -r b2800da9eb8a src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Wed Dec 20 14:53:34 2017 +0100
+++ b/src/HOL/Tools/groebner.ML	Wed Dec 20 19:17:37 2017 +0100
@@ -899,7 +899,7 @@
   | Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => find_args bounds tm
   | Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _ => find_args bounds tm
   | Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _ => find_args bounds tm
-  | \<^term>\<open>op \<Longrightarrow>\<close> $_$_ => find_args bounds tm
+  | \<^term>\<open>Pure.imp\<close> $_$_ => find_args bounds tm
   | Const("op ==",_)$_$_ => find_args bounds tm  (* FIXME proper const name *)
   | \<^term>\<open>Trueprop\<close>$_ => find_term bounds (Thm.dest_arg tm)
   | _ => raise TERM ("find_term", []))