--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Nov 26 20:05:34 2014 +0100
@@ -578,7 +578,7 @@
val n = Thm.nprems_of coind;
val m = Thm.nprems_of (hd rel_monos) - n;
fun mk_inst phi = (phi, mk_union (phi, HOLogic.eq_const (fst (dest_pred2T (fastype_of phi)))))
- |> pairself (certify ctxt);
+ |> apply2 (certify ctxt);
val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map (mk_inst o Var);
fun mk_unfold rel_eq rel_mono =
let