src/HOL/Tools/BNF/bnf_gfp_grec.ML

         SOME mapf => mapf
       | NONE => the (find_first (fn f => domain_type (fastype_of f) = T) fs));
 
     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;
 
 fun derive_natural_by_unfolding ctxt live_AsBs preT pre_map fs f const map_thms =