1.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Apr 10 14:40:11 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Apr 10 15:14:38 2014 +0200
     1.3 @@ -112,7 +112,6 @@
     1.4  
     1.5      fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs;
     1.6      val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs);
     1.7 -    val (dead_params, dead_params') = `(map Term.dest_TFree) (subtract (op =) passiveAs params');
     1.8      val FTsAs = mk_FTs allAs;
     1.9      val FTsBs = mk_FTs allBs;
    1.10      val FTsCs = mk_FTs allCs;
    1.11 @@ -157,6 +156,7 @@
    1.12      val bds = map3 mk_bd_of_bnf Dss Ass bnfs;
    1.13      val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
    1.14      val sum_bdT = fst (dest_relT (fastype_of sum_bd));
    1.15 +    val (sum_bdT_params, sum_bdT_params') = `(map TFree) (Term.add_tfreesT sum_bdT []);
    1.16  
    1.17      val ((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), z's), (ys, ys')),
    1.18        Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy),
    1.19 @@ -718,10 +718,10 @@
    1.20            val sbdT_bind = mk_internal_b sum_bdTN;
    1.21  
    1.22            val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
    1.23 -            typedef (sbdT_bind, dead_params, NoSyn)
    1.24 +            typedef (sbdT_bind, sum_bdT_params', NoSyn)
    1.25                (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
    1.26  
    1.27 -          val sbdT = Type (sbdT_name, dead_params');
    1.28 +          val sbdT = Type (sbdT_name, sum_bdT_params);
    1.29            val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
    1.30  
    1.31            val sbd_bind = mk_internal_b sum_bdN;

     2.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Apr 10 14:40:11 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Apr 10 15:14:38 2014 +0200
     2.3 @@ -82,7 +82,6 @@
     2.4  
     2.5      fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs;
     2.6      val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs);
     2.7 -    val (dead_params, dead_params') = `(map Term.dest_TFree) (subtract (op =) passiveAs params');
     2.8      val FTsAs = mk_FTs allAs;
     2.9      val FTsBs = mk_FTs allBs;
    2.10      val FTsCs = mk_FTs allCs;
    2.11 @@ -448,6 +447,7 @@
    2.12  
    2.13      val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
    2.14      val sum_bdT = fst (dest_relT (fastype_of sum_bd));
    2.15 +    val (sum_bdT_params, sum_bdT_params') = `(map TFree) (Term.add_tfreesT sum_bdT []);
    2.16  
    2.17      val (lthy, sbd, sbd_Cinfinite, sbd_Card_order, set_sbdss, in_sbds) =
    2.18        if n = 1
    2.19 @@ -457,10 +457,10 @@
    2.20            val sbdT_bind = mk_internal_b sum_bdTN;
    2.21  
    2.22            val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
    2.23 -            typedef (sbdT_bind, dead_params, NoSyn)
    2.24 +            typedef (sbdT_bind, sum_bdT_params', NoSyn)
    2.25                (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
    2.26  
    2.27 -          val sbdT = Type (sbdT_name, dead_params');
    2.28 +          val sbdT = Type (sbdT_name, sum_bdT_params);
    2.29            val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
    2.30  
    2.31            val sbd_bind = mk_internal_b sum_bdN;
    2.32 @@ -1381,14 +1381,15 @@
    2.33              let
    2.34                val sum_bd0 = Library.foldr1 (uncurry mk_csum) bd0s;
    2.35                val sum_bd0T = fst (dest_relT (fastype_of sum_bd0));
    2.36 +              val (sum_bd0T_params, sum_bd0T_params') = `(map TFree) (Term.add_tfreesT sum_bd0T []);
    2.37  
    2.38                val sbd0T_bind = mk_internal_b (sum_bdTN ^ "0");
    2.39      
    2.40                val ((sbd0T_name, (sbd0T_glob_info, sbd0T_loc_info)), lthy) =
    2.41 -                typedef (sbd0T_bind, dead_params, NoSyn)
    2.42 +                typedef (sbd0T_bind, sum_bd0T_params', NoSyn)
    2.43                    (HOLogic.mk_UNIV sum_bd0T) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
    2.44      
    2.45 -              val sbd0T = Type (sbd0T_name, dead_params');
    2.46 +              val sbd0T = Type (sbd0T_name, sum_bd0T_params);
    2.47                val Abs_sbd0T = Const (#Abs_name sbd0T_glob_info, sum_bd0T --> sbd0T);
    2.48      
    2.49                val sbd0_bind = mk_internal_b (sum_bdN ^ "0");