diff -r f6d0578b46c9 -r 8d7cb22482e3 src/HOL/Tools/BNF/bnf_lfp_countable.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_countable.ML	Wed Dec 21 11:45:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML	Wed Dec 21 12:49:15 2016 +0100
@@ -106,7 +106,7 @@
         NONE
       else if exists_subtype_in fpTs T then
         let val U = mk_U T in
-          SOME (mk_to_nat_checked U $ (build_map ctxt [] (snd_const o fst) (T, U) $ Bound j))
+          SOME (mk_to_nat_checked U $ (build_map ctxt [] [] (snd_const o fst) (T, U) $ Bound j))
         end
       else
         SOME (mk_to_nat_checked T $ Bound j);