# HG changeset patch
# User blanchet
# Date 1346418243 -7200
# Node ID 7d9631754bba63d381fc2e87695cfec3c82c5641
# Parent  c4a34ae5504d8d16acc71cd3fd97f2c72682066b
minor fixes (for compatibility with existing datatype package)

diff -r c4a34ae5504d -r 7d9631754bba src/HOL/Codatatype/Tools/bnf_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Fri Aug 31 15:04:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Fri Aug 31 15:04:03 2012 +0200
@@ -185,7 +185,7 @@
           end;
 
         val other_half_distinct_thms = map (fn thm => thm RS not_sym) half_distinct_thms;
-        val distinct_thms = half_distinct_thms @ other_half_distinct_thms;
+        val distinct_thms = interleave half_distinct_thms other_half_distinct_thms;
 
         val nchotomy_thm =
           let
@@ -255,7 +255,7 @@
             val other_half_thms =
               map2 (prove o mk_other_half_disc_disjoint_tac) half_thms goal_other_halves;
           in
-            half_thms @ other_half_thms
+            interleave half_thms other_half_thms
           end;
 
         val disc_exhaust_thm =
@@ -297,7 +297,7 @@
         val (case_cong_thm, weak_case_cong_thm) =
           let
             fun mk_prem xctr xs f g =
-              fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr),
+              fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (w, xctr),
                 mk_Trueprop_eq (f, g)));
 
             val v_eq_w = mk_Trueprop_eq (v, w);
diff -r c4a34ae5504d -r 7d9631754bba src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Fri Aug 31 15:04:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Fri Aug 31 15:04:03 2012 +0200
@@ -76,7 +76,7 @@
   rtac exhaust' 1 THEN
   ALLGOALS (hyp_subst_tac THEN'
     simp_tac (ss_only (@{thms simp_thms} @ case_thms @ injects @ distincts) HOL_basic_ss)) THEN
-  ALLGOALS (blast_tac ctxt);
+  ALLGOALS (blast_tac naked_ctxt);
 
 val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};