src/HOL/Tools/groebner.ML

 
  fun getname v = case Thm.term_of v of
   Free(s,_) => s
  | Var ((s,_),_) => s
  | _ => "x"
- fun mk_eq s t = Thm.apply (Thm.apply \<^cterm>\<open>op \<equiv> :: bool \<Rightarrow> _\<close> s) t
+ fun mk_eq s t = Thm.apply (Thm.apply \<^cterm>\<open>(\<equiv>) :: bool \<Rightarrow> _\<close> s) t
  fun mk_exists ctxt v th = Drule.arg_cong_rule (ext ctxt (Thm.typ_of_cterm v))
    (Thm.abstract_rule (getname v) v th)
  fun simp_ex_conv ctxt =
    Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)})
 

           in if null gvs then lvs else tm::acc
           end
     else tm::acc ;
 
 fun grobify_term vars tm =
-((if not (member (op aconvc) vars tm) then raise CTERM ("Not a variable", [tm]) else
+((if not (member (aconvc) vars tm) then raise CTERM ("Not a variable", [tm]) else
      [(@1, map (fn i => if i aconvc tm then 1 else 0) vars)])
 handle  CTERM _ =>
  ((let val x = dest_const tm
  in if x = @0 then [] else [(x,map (K 0) vars)]
  end)

   val (vars,bod) = strip_exists tm
   val cjs = striplist (dest_binary \<^cterm>\<open>HOL.conj\<close>) bod
   val th1 = (the (get_first (try (isolate_variable vars)) cjs)
              handle Option.Option => raise CTERM ("unwind_polys_conv",[tm]))
   val eq = Thm.lhs_of th1
-  val bod' = list_mk_binop \<^cterm>\<open>HOL.conj\<close> (eq::(remove op aconvc eq cjs))
+  val bod' = list_mk_binop \<^cterm>\<open>HOL.conj\<close> (eq::(remove (aconvc) eq cjs))
   val th2 = conj_ac_rule (mk_eq bod bod')
   val th3 =
     Thm.transitive th2
       (Drule.binop_cong_rule \<^cterm>\<open>HOL.conj\<close> th1
         (Thm.reflexive (Thm.dest_arg (Thm.rhs_of th2))))

   | Const (\<^const_name>\<open>Ex\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm)
   | 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>Pure.imp\<close> $_$_ => find_args bounds tm
-  | Const("op ==",_)$_$_ => find_args bounds tm  (* FIXME proper const name *)
+  | Const("(==)",_)$_$_ => find_args bounds tm  (* FIXME proper const name *)
   | \<^term>\<open>Trueprop\<close>$_ => find_term bounds (Thm.dest_arg tm)
   | _ => raise TERM ("find_term", []))
 and find_args bounds tm =
   let val (t, u) = Thm.dest_binop tm
   in (find_term bounds t handle TERM _ => find_term bounds u) end