1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 21:44:43 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 11 09:40:05 2012 +0200
     1.3 @@ -367,7 +367,7 @@
     1.4  
     1.5          val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
     1.6  
     1.7 -        fun some_lfp_sugar ((selss, discIs, sel_thmss), no_defs_lthy) =
     1.8 +        fun some_lfp_sugar ((selss0, discIs, sel_thmss), no_defs_lthy) =
     1.9            let
    1.10              val fpT_to_C = fpT --> C;
    1.11  
    1.12 @@ -402,11 +402,11 @@
    1.13  
    1.14              val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
    1.15            in
    1.16 -            ((ctrs, selss, iter, recx, v, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def),
    1.17 +            ((ctrs, selss0, iter, recx, v, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def),
    1.18               lthy)
    1.19            end;
    1.20  
    1.21 -        fun some_gfp_sugar ((selss, discIs, sel_thmss), no_defs_lthy) =
    1.22 +        fun some_gfp_sugar ((selss0, discIs, sel_thmss), no_defs_lthy) =
    1.23            let
    1.24              val B_to_fpT = C --> fpT;
    1.25  
    1.26 @@ -445,7 +445,7 @@
    1.27  
    1.28              val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts;
    1.29            in
    1.30 -            ((ctrs, selss, coiter, corec, v, xss, ctr_defs, discIs, sel_thmss, coiter_def,
    1.31 +            ((ctrs, selss0, coiter, corec, v, xss, ctr_defs, discIs, sel_thmss, coiter_def,
    1.32                corec_def), lthy)
    1.33            end;
    1.34        in
    1.35 @@ -594,21 +594,22 @@
    1.36          val disc_coiter_thmss = map2 mk_disc_coiter_like_thms coiter_thmss discIss;
    1.37          val disc_corec_thmss = map2 mk_disc_coiter_like_thms corec_thmss discIss;
    1.38  
    1.39 -        fun mk_sel_coiter_like_thm coiter_like_thm sel sel_thm =
    1.40 +        fun mk_sel_coiter_like_thm coiter_like_thm sel0 sel_thm =
    1.41            let
    1.42 -            val (domT, ranT) = dest_funT (fastype_of sel);
    1.43 +            val (domT, ranT) = dest_funT (fastype_of sel0);
    1.44              val arg_cong' =
    1.45                Drule.instantiate' (map (SOME o certifyT lthy) [domT, ranT])
    1.46 -                [NONE, NONE, SOME (certify lthy sel)] arg_cong;
    1.47 +                [NONE, NONE, SOME (certify lthy sel0)] arg_cong
    1.48 +              |> Thm.varifyT_global;
    1.49              val sel_thm' = sel_thm RSN (2, trans);
    1.50            in
    1.51 -            (coiter_like_thm RS arg_cong') RS sel_thm'
    1.52 +            coiter_like_thm RS arg_cong' RS sel_thm'
    1.53            end;
    1.54  
    1.55          val sel_coiter_thmsss =
    1.56            map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss sel_thmsss;
    1.57          val sel_corec_thmsss =
    1.58 -          map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss sel_thmsss;
    1.59 +          map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss sel_thmsss;
    1.60  
    1.61          val notes =
    1.62            [(coitersN, coiter_thmss),