normalize schematic names since they are used to instantiate the theorem later

--- 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;