--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Sun Jul 05 15:02:30 2015 +0200
@@ -607,9 +607,9 @@
let
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)))))
- |> apply2 (Thm.cterm_of ctxt);
- val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map (mk_inst o Var);
+ fun mk_inst phi =
+ (phi, Thm.cterm_of ctxt (mk_union (Var phi, HOLogic.eq_const (fst (dest_pred2T (#2 phi))))))
+ val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map mk_inst;
fun mk_unfold rel_eq rel_mono =
let
val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl];