tuned;

--- a/src/HOL/Decision_Procs/Cooper.thy	Tue Oct 30 22:59:06 2018 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Oct 31 14:47:59 2018 +0100
@@ -2507,12 +2507,12 @@
     (case t of
       (l as f $ a) $ b =>
         if is_ty t orelse is_op t then term_bools (term_bools acc l) b
-        else insert (aconv) t acc
+        else insert (op aconv) t acc
     | f $ a =>
         if is_ty t orelse is_op t then term_bools (term_bools acc f) a
-        else insert (aconv) t acc
+        else insert (op aconv) t acc
     | Abs p => term_bools acc (snd (Syntax_Trans.variant_abs p))  (* FIXME !? *)
-    | _ => if is_ty t orelse is_op t then acc else insert (aconv) t acc)
+    | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc)
   end;
 
 in

--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Oct 30 22:59:06 2018 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Oct 31 14:47:59 2018 +0100
@@ -4066,7 +4066,7 @@
 fun frpar_procedure alternative T ps fm =
   let
     val frpar = if alternative then @{code frpar2} else @{code frpar};
-    val fs = subtract (aconv) (map Free (Term.add_frees fm [])) ps;
+    val fs = subtract (op aconv) (map Free (Term.add_frees fm [])) ps;
     val eval = term_of_fm T fs ps o frpar o fm_of_term fs ps;
     val t = HOLogic.dest_Trueprop fm;
   in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, eval t)) end;