src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
changeset 49125 5fc5211cf104
parent 49124 968e1b7de057
child 49126 1bbd7a37fc29
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 15:51:32 2012 +0200
@@ -166,13 +166,21 @@
             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
           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';
+
         (* ### *)
         fun cheat_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
 
-        val exhaust_tac = cheat_tac;
-
         val inject_tacss = map (fn 0 => [] | _ => [cheat_tac]) ms;
 
         val half_distinct_tacss = map (map (K cheat_tac)) (mk_half_pairss ks);