diff -r 644f0d4820a1 -r ba2fa4e99729 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Apr 28 00:54:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Apr 28 00:54:30 2014 +0200
@@ -2438,7 +2438,8 @@
               (SOME deads) map_b rel_b set_bs consts
             #> (fn (bnf, lthy) => (bnf, register_bnf (Local_Theory.full_name lthy b) bnf lthy)))
           bs tacss map_bs rel_bs set_bss wit_thmss
-          ((((((bs ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ all_witss) ~~ map SOME Jrels)
+          ((((((replicate n Binding.empty ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~
+            all_witss) ~~ map SOME Jrels)
           lthy;
 
         val timer = time (timer "registered new codatatypes as BNFs");