# HG changeset patch
# User traytel
# Date 1469779402 -7200
# Node ID 91f03f3b64703305366e165e6515566fb1393f09
# Parent  eca71be9c94874ab9abfef65a39de4bfa204a8b7
made generation of transfer goals more robust w.r.t. dead variables

diff -r eca71be9c948 -r 91f03f3b6470 src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Fri Jul 29 15:00:51 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Fri Jul 29 10:03:22 2016 +0200
@@ -87,12 +87,16 @@
       |> mk_TFrees' (map snd skematic_Ts)
       ||>> mk_TFrees' (map snd skematic_Ts);
 
-    val (Rs, names_lthy) = mk_Frees "R" (map2 mk_pred2T As Bs) names_lthy;
+    val ((Rs, Rs'), names_lthy) = mk_Frees' "R" (map2 mk_pred2T As Bs) names_lthy;
 
     val fA = Term.subst_TVars (map fst skematic_Ts ~~ As) f;
     val fB = Term.subst_TVars (map fst skematic_Ts ~~ Bs) f;
+
+    val goal = mk_parametricity_goal lthy Rs fA fB;
+    val used_Rs = Term.add_frees goal [];
+    val subst = map (dest_pred2T o snd) (filter_out (member (op =) used_Rs) Rs');
   in
-    (mk_parametricity_goal lthy Rs fA fB, names_lthy)
+    (goal |> Term.subst_atomic_types subst, names_lthy)
   end;
 
 fun fp_rec_sugar_transfer_interpretation prove {transfers, fun_names, funs, fun_defs, fpTs} =