# HG changeset patch
# User blanchet
# Date 1370546524 -7200
# Node ID a74e0a4741df958a56cae7e38df7d1c7b058df3c
# Parent  095c88b93e8d9db7f2f1c63c2d1ae4b197ea32f0
tuning

diff -r 095c88b93e8d -r a74e0a4741df src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Thu Jun 06 21:18:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Thu Jun 06 21:22:04 2013 +0200
@@ -35,81 +35,83 @@
 fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P});
 
 fun mk_nchotomy_tac n exhaust =
-  (rtac allI THEN' rtac exhaust THEN'
-   EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1;
+  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)));
 
 fun mk_unique_disc_def_tac m uexhaust =
-  EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1;
+  HEADGOAL (EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl]);
 
 fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
-  EVERY' ([rtac (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans),
+  HEADGOAL (EVERY' ([rtac (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans),
     rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
     hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
     rtac distinct, rtac uexhaust] @
     (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
-     |> k = 1 ? swap |> op @)) 1;
+     |> k = 1 ? swap |> op @)));
 
 fun mk_half_disc_exclude_tac ctxt m discD disc' =
-  (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN' rtac disc') 1;
+  HEADGOAL (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
+    rtac disc');
 
-fun mk_other_half_disc_exclude_tac half = (etac @{thm contrapos_pn} THEN' etac half) 1;
+fun mk_other_half_disc_exclude_tac half = HEADGOAL (etac @{thm contrapos_pn} THEN' etac half);
 
 fun mk_disc_exhaust_tac n exhaust discIs =
-  (rtac exhaust THEN'
-   EVERY' (map2 (fn k => fn discI =>
-     dtac discI THEN' select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) discIs)) 1;
+  HEADGOAL (rtac exhaust THEN'
+    EVERY' (map2 (fn k => fn discI =>
+      dtac discI THEN' select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) discIs));
 
 fun mk_collapse_tac ctxt m discD sels =
-  (dtac discD THEN'
-   (if m = 0 then
-      atac
-    else
-      REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
-      SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)) 1;
+  HEADGOAL (dtac discD THEN'
+    (if m = 0 then
+       atac
+     else
+       REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
+       SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl));
 
 fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
     disc_excludesss' =
   if ms = [0] then
-    (rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN'
-     TRY o EVERY' [rtac udisc_exhaust, atac, rtac vdisc_exhaust, atac]) 1
+    HEADGOAL (rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN'
+      TRY o EVERY' [rtac udisc_exhaust, atac, rtac vdisc_exhaust, atac])
   else
     let val ks = 1 upto n in
-      (rtac udisc_exhaust THEN'
-       EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' =>
-           fn uuncollapse =>
-         EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac,
-           rtac sym, rtac vdisc_exhaust,
-           EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse =>
-             EVERY'
-               (if k' = k then
-                  [rtac (vuncollapse RS trans), TRY o atac] @
-                  (if m = 0 then
-                     [rtac refl]
-                   else
-                     [if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac],
-                      REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE,
-                      asm_simp_tac (ss_only [] ctxt)])
-                else
-                  [dtac (the_single (if k = n then disc_excludes else disc_excludes')),
-                   etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),
-                   atac, atac]))
-             ks disc_excludess disc_excludess' uncollapses)])
-         ks ms disc_excludesss disc_excludesss' uncollapses)) 1
+      HEADGOAL (rtac udisc_exhaust THEN'
+        EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' =>
+            fn uuncollapse =>
+          EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac,
+            rtac sym, rtac vdisc_exhaust,
+            EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse =>
+              EVERY'
+                (if k' = k then
+                   [rtac (vuncollapse RS trans), TRY o atac] @
+                   (if m = 0 then
+                      [rtac refl]
+                    else
+                      [if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac],
+                       REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE,
+                       asm_simp_tac (ss_only [] ctxt)])
+                 else
+                   [dtac (the_single (if k = n then disc_excludes else disc_excludes')),
+                    etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),
+                    atac, atac]))
+              ks disc_excludess disc_excludess' uncollapses)])
+          ks ms disc_excludesss disc_excludesss' uncollapses))
     end;
 
 fun mk_case_conv_tac ctxt n uexhaust cases discss' selss =
-  (rtac uexhaust THEN'
-   EVERY' (map3 (fn casex => fn if_discs => fn sels =>
-       EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), rtac casex])
-     cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)) 1;
+  HEADGOAL (rtac uexhaust THEN'
+    EVERY' (map3 (fn casex => fn if_discs => fn sels =>
+        EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)),
+          rtac casex])
+      cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss));
 
 fun mk_case_cong_tac ctxt uexhaust cases =
-  (rtac uexhaust THEN'
-   EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases)) 1;
+  HEADGOAL (rtac uexhaust THEN'
+    EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases));
 
 (* TODO: More precise "simp_thms"; get rid of "blast_tac" *)
 fun mk_split_tac ctxt uexhaust cases injectss distinctsss =
-  rtac uexhaust 1 THEN
+  HEADGOAL (rtac uexhaust) THEN
   ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
      simp_tac (ss_only (@{thms simp_thms} @ cases @ nth injectss (k - 1) @
        flat (nth distinctsss (k - 1))) ctxt)) k) THEN
@@ -118,6 +120,7 @@
 val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
 
 fun mk_split_asm_tac ctxt split =
-  rtac (split RS trans) 1 THEN unfold_thms_tac ctxt split_asm_thms THEN rtac refl 1;
+  HEADGOAL (rtac (split RS trans)) THEN unfold_thms_tac ctxt split_asm_thms THEN
+  HEADGOAL (rtac refl);
 
 end;