# HG changeset patch
# User blanchet
# Date 1411585207 -7200
# Node ID a379d4531d1a98193006fbd688e0987d2bc7c281
# Parent  2fa300429c1134839f616190c029ef0091e8ac0e
avoid type variable name clash

diff -r 2fa300429c11 -r a379d4531d1a src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 24 21:00:07 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 24 21:00:07 2014 +0200
@@ -425,6 +425,7 @@
       val fTs = map (op -->) live_AsBs;
 
       val (((((((([C, E], xss), yss), fs), Rs), ta), tb), thesis), names_lthy) = lthy
+        |> fold (fold Variable.declare_typ) [As, Bs]
         |> mk_TFrees 2
         ||>> mk_Freess "x" ctr_Tss
         ||>> mk_Freess "y" (map (map B_ify) ctr_Tss)
@@ -713,11 +714,10 @@
 
       val case_transfer_thms =
         let
-          val (R, names_lthy) = yield_singleton (mk_Frees "R") (mk_pred2T C E) names_lthy;
-
+          val (S, names_lthy) = yield_singleton (mk_Frees "S") (mk_pred2T C E) names_lthy;
           val caseA = mk_case As C casex;
           val caseB = mk_case Bs E casex;
-          val goal = mk_parametricity_goal names_lthy (R :: Rs) caseA caseB;
+          val goal = mk_parametricity_goal names_lthy (S :: Rs) caseA caseB;
         in
           Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
             mk_case_transfer_tac ctxt rel_cases_thm case_thms)