diff -r f4b6e2626cf8 -r 894d613f7f7c src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Wed Dec 10 20:56:33 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Thu Dec 11 14:01:40 2014 +0100
@@ -925,8 +925,10 @@
               in qualify' o Binding.qualify true namei end;
             val odead = dead_of_bnf bnf;
             val olive = live_of_bnf bnf;
-            val oDs_pos = find_indices op = [TFree ("dead", [])] (snd (Term.dest_Type
-              (mk_T_of_bnf (replicate odead (TFree ("dead", []))) (replicate olive dummyT) bnf)));
+            val Ds = map (fn i => TFree (string_of_int i, [])) (1 upto odead);
+            val Us = snd (Term.dest_Type (mk_T_of_bnf Ds (replicate olive dummyT) bnf));
+            val oDs_pos = map (fn x => find_index (fn y => x = y) Us) Ds
+              |> filter (fn x => x >= 0);
             val oDs = map (nth Ts) oDs_pos;
             val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
             val ((inners, (Dss, Ass)), (accum', lthy')) =