# HG changeset patch
# User blanchet
# Date 1346794953 -7200
# Node ID de13b454fa315586504941dd91d57a8f1f7249a8
# Parent  846264f80f16623c67eda84f7f936e4bcac6b716
fixed some type issues in sugar "exhaust_tac"

diff -r 846264f80f16 -r de13b454fa31 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 23:09:08 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 23:42:33 2012 +0200
@@ -124,7 +124,7 @@
     val unfs = map (mk_unf As) raw_unfs;
     val flds = map (mk_fld As) raw_flds;
 
-    fun pour_some_sugar_on_type ((((((((((b, T), fld), unf), fld_unf), unf_fld), fld_inject),
+    fun pour_sugar_on_type ((((((((((b, T), fld), unf), fld_unf), unf_fld), fld_inject),
         ctr_binders), ctr_Tss), disc_binders), sel_binderss) no_defs_lthy =
       let
         val n = length ctr_binders;
@@ -168,27 +168,29 @@
         val ctrs = map (Morphism.term phi) raw_ctrs;
         val casex = Morphism.term phi raw_case;
 
-        val fld_iff_unf_thm =
+        fun exhaust_tac {context = ctxt, ...} =
           let
-            val goal =
-              fold_rev Logic.all [u, v]
-                (mk_Trueprop_eq (HOLogic.mk_eq (v, fld $ u), HOLogic.mk_eq (unf $ v, u)));
+            val fld_iff_unf_thm =
+              let
+                val goal =
+                  fold_rev Logic.all [u, v]
+                    (mk_Trueprop_eq (HOLogic.mk_eq (v, fld $ u), HOLogic.mk_eq (unf $ v, u)));
+              in
+                Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+                  mk_fld_iff_unf_tac ctxt (map (SOME o certifyT lthy) [unf_T, T]) (certify lthy fld)
+                    (certify lthy unf) fld_unf unf_fld)
+                |> Thm.close_derivation
+                |> Morphism.thm phi
+              end;
+
+            val sumEN_thm' =
+              Local_Defs.unfold lthy @{thms all_unit_eq}
+                (Drule.instantiate' (map (SOME o certifyT lthy) prod_Ts) [] (mk_sumEN n))
+              |> Morphism.thm phi;
           in
-            Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
-              mk_fld_iff_unf_tac ctxt (map (SOME o certifyT lthy) [unf_T, T]) (certify lthy fld)
-                (certify lthy unf) fld_unf unf_fld)
-            |> Thm.close_derivation
+            mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf_thm sumEN_thm'
           end;
 
-        val sumEN_thm = mk_sumEN n;
-        val sumEN_thm' =
-          let val cTs = map (SOME o certifyT lthy) prod_Ts in
-            Local_Defs.unfold lthy @{thms all_unit_eq} (Drule.instantiate' cTs [] sumEN_thm)
-          end;
-
-        fun exhaust_tac {context = ctxt, ...} =
-          mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf_thm sumEN_thm';
-
         val inject_tacss =
           map2 (fn 0 => K []
                  | _ => fn ctr_def => [fn {context = ctxt, ...} =>
@@ -228,7 +230,7 @@
       end;
   in
     lthy'
-    |> fold pour_some_sugar_on_type (bs ~~ Ts ~~ flds ~~ unfs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~
+    |> fold pour_sugar_on_type (bs ~~ Ts ~~ flds ~~ unfs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~
       ctr_binderss ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss)
   end;
 
diff -r 846264f80f16 -r de13b454fa31 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 23:09:08 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 23:42:33 2012 +0200
@@ -28,12 +28,10 @@
    rtac refl) 1;
 
 fun mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf sumEN' =
-  Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN
-  rtac sumEN' 1 THEN
+  Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN
   Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN
-  EVERY' (map2 (fn k => fn m =>
-     select_prem_tac n (REPEAT_DETERM_N m o dtac @{thm meta_spec} THEN' etac @{thm meta_mp}) k THEN'
-     atac) (1 upto n) ms) 1;
+  EVERY' (map2 (fn k => fn m => select_prem_tac n (REPEAT_DETERM_N m o dtac @{thm meta_spec} THEN'
+    etac @{thm meta_mp}) k THEN' atac) (1 upto n) ms) 1;
 
 fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
   (rtac iffI THEN'
@@ -47,9 +45,7 @@
   rtac @{thm sum.distinct(1)} 1;
 
 fun mk_inject_tac ctxt ctr_def fld_inject =
-  Local_Defs.unfold_tac ctxt [ctr_def] THEN
-  rtac (fld_inject RS ssubst) 1 THEN
-  Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN
-  rtac refl 1;
+  Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN
+  Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
 
 end;