# HG changeset patch
# User traytel
# Date 1458286357 -3600
# Node ID d23be25c08358098ef10f9d6db61e45294ffbbfd
# Parent  ee48e0b4f6699581495ecdb459705399066301d3
normalize schematic names since they are used to instantiate the theorem later

diff -r ee48e0b4f669 -r d23be25c0835 src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- 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;