# HG changeset patch
# User traytel
# Date 1348761693 -7200
# Node ID 7db3d29868814e08c2cac483de3043a3e893d848
# Parent  0e248756147a4ad114cd4c18eb24fa493c132919
type of the bound of a BNF depends at most on dead type variables

diff -r 0e248756147a -r 7db3d2986881 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Sep 27 17:54:35 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Sep 27 18:01:33 2012 +0200
@@ -104,6 +104,7 @@
 
     fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs;
     val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs);
+    val (dead_params, dead_params') = `(map Term.dest_TFree) (subtract (op =) passiveAs params');
     val FTsAs = mk_FTs allAs;
     val FTsBs = mk_FTs allBs;
     val FTsCs = mk_FTs allCs;
@@ -1022,10 +1023,10 @@
           val sbdT_bind = Binding.suffix_name ("_" ^ sum_bdTN) b;
 
           val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
-            typedef false NONE (sbdT_bind, params, NoSyn)
+            typedef false NONE (sbdT_bind, dead_params, NoSyn)
               (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
 
-          val sbdT = Type (sbdT_name, params');
+          val sbdT = Type (sbdT_name, dead_params');
           val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
 
           val sbd_bind = Binding.suffix_name ("_" ^ sum_bdN) b;