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