src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy

   | term_of_fm T fs ps _ = error "term_of_fm: quantifiers";
 
 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;
 
 in