# HG changeset patch
# User blanchet
# Date 1347349205 -7200
# Node ID c96a07255e107f08e0d3811f230fd4e3992de3eb
# Parent  70ffce5b65a4936fc472cd3b7ff787c77e6ac8a8
correctly generate sel_coiter and sel_corec theorems

diff -r 70ffce5b65a4 -r c96a07255e10 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 21:44:43 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 11 09:40:05 2012 +0200
@@ -367,7 +367,7 @@
 
         val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
 
-        fun some_lfp_sugar ((selss, discIs, sel_thmss), no_defs_lthy) =
+        fun some_lfp_sugar ((selss0, discIs, sel_thmss), no_defs_lthy) =
           let
             val fpT_to_C = fpT --> C;
 
@@ -402,11 +402,11 @@
 
             val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
           in
-            ((ctrs, selss, iter, recx, v, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def),
+            ((ctrs, selss0, iter, recx, v, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def),
              lthy)
           end;
 
-        fun some_gfp_sugar ((selss, discIs, sel_thmss), no_defs_lthy) =
+        fun some_gfp_sugar ((selss0, discIs, sel_thmss), no_defs_lthy) =
           let
             val B_to_fpT = C --> fpT;
 
@@ -445,7 +445,7 @@
 
             val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts;
           in
-            ((ctrs, selss, coiter, corec, v, xss, ctr_defs, discIs, sel_thmss, coiter_def,
+            ((ctrs, selss0, coiter, corec, v, xss, ctr_defs, discIs, sel_thmss, coiter_def,
               corec_def), lthy)
           end;
       in
@@ -594,21 +594,22 @@
         val disc_coiter_thmss = map2 mk_disc_coiter_like_thms coiter_thmss discIss;
         val disc_corec_thmss = map2 mk_disc_coiter_like_thms corec_thmss discIss;
 
-        fun mk_sel_coiter_like_thm coiter_like_thm sel sel_thm =
+        fun mk_sel_coiter_like_thm coiter_like_thm sel0 sel_thm =
           let
-            val (domT, ranT) = dest_funT (fastype_of sel);
+            val (domT, ranT) = dest_funT (fastype_of sel0);
             val arg_cong' =
               Drule.instantiate' (map (SOME o certifyT lthy) [domT, ranT])
-                [NONE, NONE, SOME (certify lthy sel)] arg_cong;
+                [NONE, NONE, SOME (certify lthy sel0)] arg_cong
+              |> Thm.varifyT_global;
             val sel_thm' = sel_thm RSN (2, trans);
           in
-            (coiter_like_thm RS arg_cong') RS sel_thm'
+            coiter_like_thm RS arg_cong' RS sel_thm'
           end;
 
         val sel_coiter_thmsss =
           map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss sel_thmsss;
         val sel_corec_thmsss =
-          map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss sel_thmsss;
+          map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss sel_thmsss;
 
         val notes =
           [(coitersN, coiter_thmss),