src/HOL/Codatatype/Tools/bnf_gfp.ML
changeset 49228 e43910ccee74
parent 49225 a9295b1f401b
child 49231 43d2df313559
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sun Sep 09 10:15:58 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sun Sep 09 10:58:11 2012 +0200
     1.3 @@ -1028,7 +1028,7 @@
     1.4            val sbdT_bind = Binding.suffix_name ("_" ^ sum_bdTN) b;
     1.5  
     1.6            val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
     1.7 -            typedef true NONE (sbdT_bind, params, NoSyn)
     1.8 +            typedef false NONE (sbdT_bind, params, NoSyn)
     1.9                (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
    1.10  
    1.11            val sbdT = Type (sbdT_name, params');
    1.12 @@ -1052,12 +1052,8 @@
    1.13            val sbd_def = Morphism.thm phi sbd_def_free;
    1.14            val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT));
    1.15  
    1.16 -          val sbdT_set_def = the (#set_def sbdT_loc_info);
    1.17 -          val sbdT_Abs_inject = #Abs_inject sbdT_loc_info;
    1.18 -          val sbdT_Abs_cases = #Abs_cases sbdT_loc_info;
    1.19 -
    1.20 -          val Abs_sbdT_inj = mk_Abs_inj_thm sbdT_set_def sbdT_Abs_inject;
    1.21 -          val Abs_sbdT_bij = mk_Abs_bij_thm lthy sbdT_set_def sbdT_Abs_inject sbdT_Abs_cases;
    1.22 +          val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
    1.23 +          val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info);
    1.24  
    1.25            fun mk_sum_Cinfinite [thm] = thm
    1.26              | mk_sum_Cinfinite (thm :: thms) =