# HG changeset patch # User traytel # Date 1397135678 -7200 # Node ID a13c2ccc160b7622642b0e0e38dd9bc4699df0e3 # Parent b62c4e6d1b556fda14aaac305aa2df0e240338a3 more accurate type arguments for intermeadiate typedefs diff -r b62c4e6d1b55 -r a13c2ccc160b src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Apr 10 14:40:11 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Apr 10 15:14:38 2014 +0200 @@ -112,7 +112,6 @@ 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; @@ -157,6 +156,7 @@ val bds = map3 mk_bd_of_bnf Dss Ass bnfs; val sum_bd = Library.foldr1 (uncurry mk_csum) bds; val sum_bdT = fst (dest_relT (fastype_of sum_bd)); + val (sum_bdT_params, sum_bdT_params') = `(map TFree) (Term.add_tfreesT sum_bdT []); val ((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), z's), (ys, ys')), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy), @@ -718,10 +718,10 @@ val sbdT_bind = mk_internal_b sum_bdTN; val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) = - typedef (sbdT_bind, dead_params, NoSyn) + typedef (sbdT_bind, sum_bdT_params', NoSyn) (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; - val sbdT = Type (sbdT_name, dead_params'); + val sbdT = Type (sbdT_name, sum_bdT_params); val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT); val sbd_bind = mk_internal_b sum_bdN; diff -r b62c4e6d1b55 -r a13c2ccc160b src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Apr 10 14:40:11 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Apr 10 15:14:38 2014 +0200 @@ -82,7 +82,6 @@ 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; @@ -448,6 +447,7 @@ val sum_bd = Library.foldr1 (uncurry mk_csum) bds; val sum_bdT = fst (dest_relT (fastype_of sum_bd)); + val (sum_bdT_params, sum_bdT_params') = `(map TFree) (Term.add_tfreesT sum_bdT []); val (lthy, sbd, sbd_Cinfinite, sbd_Card_order, set_sbdss, in_sbds) = if n = 1 @@ -457,10 +457,10 @@ val sbdT_bind = mk_internal_b sum_bdTN; val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) = - typedef (sbdT_bind, dead_params, NoSyn) + typedef (sbdT_bind, sum_bdT_params', NoSyn) (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; - val sbdT = Type (sbdT_name, dead_params'); + val sbdT = Type (sbdT_name, sum_bdT_params); val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT); val sbd_bind = mk_internal_b sum_bdN; @@ -1381,14 +1381,15 @@ let val sum_bd0 = Library.foldr1 (uncurry mk_csum) bd0s; val sum_bd0T = fst (dest_relT (fastype_of sum_bd0)); + val (sum_bd0T_params, sum_bd0T_params') = `(map TFree) (Term.add_tfreesT sum_bd0T []); val sbd0T_bind = mk_internal_b (sum_bdTN ^ "0"); val ((sbd0T_name, (sbd0T_glob_info, sbd0T_loc_info)), lthy) = - typedef (sbd0T_bind, dead_params, NoSyn) + typedef (sbd0T_bind, sum_bd0T_params', NoSyn) (HOLogic.mk_UNIV sum_bd0T) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; - val sbd0T = Type (sbd0T_name, dead_params'); + val sbd0T = Type (sbd0T_name, sum_bd0T_params); val Abs_sbd0T = Const (#Abs_name sbd0T_glob_info, sum_bd0T --> sbd0T); val sbd0_bind = mk_internal_b (sum_bdN ^ "0");