--- 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