--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Wed Dec 21 11:45:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Wed Dec 21 12:49:15 2016 +0100
@@ -1005,8 +1005,8 @@
val simple_Ts = map fst simple_T_mapfs;
- val t_map = build_map ctxt simple_Ts build_simple (apply2 (range_type o fastype_of) (t, u));
- val u_map = build_map ctxt simple_Ts build_simple (apply2 (domain_type o fastype_of) (t, u));
+ val t_map = build_map ctxt simple_Ts [] build_simple (apply2 (range_type o fastype_of) (t, u));
+ val u_map = build_map ctxt simple_Ts [] build_simple (apply2 (domain_type o fastype_of) (t, u));
in
mk_Trueprop_eq (HOLogic.mk_comp (u, u_map), HOLogic.mk_comp (t_map, t))
end;