# HG changeset patch
# User blanchet
# Date 1389361177 -3600
# Node ID b4b82802588017071a786cbbedc1f41915cf6835
# Parent  891141de56721186b379fc5a25d6ebfe9222f2e5
tuning

diff -r 891141de5672 -r b4b828025880 src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Fri Jan 10 14:39:37 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Fri Jan 10 14:39:37 2014 +0100
@@ -88,25 +88,25 @@
   HEADGOAL (if m = 0 then rtac TrueI
     else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' case_atac ctxt) THEN' case_atac ctxt);
 
-fun different_case_tac ctxt m excl =
+fun different_case_tac ctxt m exclude =
   HEADGOAL (if m = 0 then
       mk_primcorec_assumption_tac ctxt []
     else
-      dtac excl THEN' (REPEAT_DETERM_N (m - 1) o case_atac ctxt) THEN'
+      dtac exclude THEN' (REPEAT_DETERM_N (m - 1) o case_atac ctxt) THEN'
       mk_primcorec_assumption_tac ctxt []);
 
-fun cases_tac ctxt k m exclsss =
-  let val n = length exclsss in
+fun cases_tac ctxt k m excludesss =
+  let val n = length excludesss in
     EVERY (map (fn [] => if k = n then all_tac else same_case_tac ctxt m
-        | [excl] => different_case_tac ctxt m excl)
-      (take k (nth exclsss (k - 1))))
+        | [exclude] => different_case_tac ctxt m exclude)
+      (take k (nth excludesss (k - 1))))
   end;
 
 fun prelude_tac ctxt defs thm =
   unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN unfold_thms_tac ctxt unfold_lets;
 
-fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss =
-  prelude_tac ctxt defs disc_corec THEN cases_tac ctxt k m exclsss;
+fun mk_primcorec_disc_tac ctxt defs disc_corec k m excludesss =
+  prelude_tac ctxt defs disc_corec THEN cases_tac ctxt k m excludesss;
 
 fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss
     disc_excludes =
@@ -124,9 +124,9 @@
     resolve_tac (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac);
 
 fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_idents map_comps fun_sel k
-    m exclsss =
+    m excludesss =
   prelude_tac ctxt defs (fun_sel RS trans) THEN
-  cases_tac ctxt k m exclsss THEN
+  cases_tac ctxt k m excludesss THEN
   HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE'
     eresolve_tac falseEs ORELSE'
     resolve_tac split_connectI ORELSE'