# HG changeset patch
# User blanchet
# Date 1376313916 -7200
# Node ID 3777ba39c660ddee038a785d5da74eed990b3582
# Parent  0cd62cb233e05fe43f9be4e73a9291126248894b
tuning

diff -r 0cd62cb233e0 -r 3777ba39c660 src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Mon Aug 12 09:51:00 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Mon Aug 12 15:25:16 2013 +0200
@@ -36,7 +36,7 @@
 
 fun mk_nchotomy_tac n exhaust =
   HEADGOAL (rtac allI THEN' rtac exhaust THEN'
-   EVERY'  (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n)));
+   EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n)));
 
 fun mk_unique_disc_def_tac m uexhaust =
   HEADGOAL (EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl]);
diff -r 0cd62cb233e0 -r 3777ba39c660 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Mon Aug 12 09:51:00 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Mon Aug 12 15:25:16 2013 +0200
@@ -149,7 +149,7 @@
       mss (unflat mss (1 upto n)) kkss)
   end;
 
-fun mk_coinduct_same_ctr ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels =
+fun mk_coinduct_same_ctr_tac ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels =
   hyp_subst_tac ctxt THEN'
   CONVERSION (hhf_concl_conv
     (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN'
@@ -161,7 +161,7 @@
      REPEAT o etac conjE THEN_MAYBE' REPEAT o hyp_subst_tac ctxt THEN' REPEAT o rtac conjI THEN'
      REPEAT o rtac refl);
 
-fun mk_coinduct_distinct_ctrs ctxt discs discs' =
+fun mk_coinduct_distinct_ctrs_tac ctxt discs discs' =
   hyp_subst_tac ctxt THEN' REPEAT o etac conjE THEN'
   full_simp_tac (ss_only (refl :: no_refl (discs @ discs') @ basic_simp_thms) ctxt);
 
@@ -175,9 +175,9 @@
         EVERY' ([rtac exhaust, K (inst_as_projs_tac ctxt 2)] @
           map2 (fn k' => fn discs' =>
             if k' = k then
-              mk_coinduct_same_ctr ctxt rel_eqs' pre_rel_def dtor_ctor ctr_def discs sels
+              mk_coinduct_same_ctr_tac ctxt rel_eqs' pre_rel_def dtor_ctor ctr_def discs sels
             else
-              mk_coinduct_distinct_ctrs ctxt discs discs') ks discss)) ks ctr_defs discss selss)
+              mk_coinduct_distinct_ctrs_tac ctxt discs discs') ks discss)) ks ctr_defs discss selss)
   end;
 
 fun mk_coinduct_tac ctxt rel_eqs' nn ns dtor_coinduct' pre_rel_defs dtor_ctors exhausts ctr_defss