# HG changeset patch # User wenzelm # Date 1540993679 -3600 # Node ID 74455459973ddb399d4d61e57a7df0194c8508af # Parent ab98f058f9dcc0af3abdf6bbcc9094b2607672f4 tuned; diff -r ab98f058f9dc -r 74455459973d src/HOL/Decision_Procs/Cooper.thy --- 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 diff -r ab98f058f9dc -r 74455459973d src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- 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;