--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Mar 17 14:48:14 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Fri Mar 18 08:32:37 2016 +0100
@@ -165,7 +165,7 @@
val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs;
val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #xtor_rel_co_induct)
- |> map (unfold_thms lthy (id_apply :: rel_unfolds));
+ |> map (zero_var_indexes o unfold_thms lthy (id_apply :: rel_unfolds));
val rel_defs = map rel_def_of_bnf bnfs;
val rel_monos = map rel_mono_of_bnf bnfs;