# HG changeset patch
# User blanchet
# Date 1455536890 -3600
# Node ID dc837462033236b58cebc6e5dd5cb04e5c1c9623
# Parent  6b01bff94d87b67111406e6cacd0d34c405cbb8f
tuning

diff -r 6b01bff94d87 -r dc8374620332 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Feb 15 12:47:52 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Feb 15 12:48:10 2016 +0100
@@ -2594,8 +2594,7 @@
         val (set_induct_thms, set_induct_attrss) =
           derive_set_induct_thms_for_types lthy nn fpTs (map #ctrs ctr_sugars)
             (map (map (mk_set As)) (map sets_of_bnf fp_bnfs)) dtor_set_inducts
-            (map #exhaust ctr_sugars) (flat pre_set_defss) (flat ctr_defss)
-            dtor_ctors abs_inverses
+            (map #exhaust ctr_sugars) (flat pre_set_defss) (flat ctr_defss) dtor_ctors abs_inverses
           |> split_list;
 
         val simp_thmss =
diff -r 6b01bff94d87 -r dc8374620332 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Mon Feb 15 12:47:52 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Mon Feb 15 12:48:10 2016 +0100
@@ -104,11 +104,11 @@
       (take k (nth excludesss (k - 1))))
   end;
 
-fun prelude_tac ctxt defs thm =
-  unfold_thms_tac ctxt defs THEN HEADGOAL (rtac ctxt thm) THEN unfold_thms_tac ctxt unfold_lets;
+fun prelude_tac ctxt fun_defs thm =
+  unfold_thms_tac ctxt fun_defs THEN HEADGOAL (rtac ctxt thm) THEN unfold_thms_tac ctxt unfold_lets;
 
-fun mk_primcorec_disc_tac ctxt defs corec_disc k m excludesss =
-  prelude_tac ctxt defs corec_disc THEN cases_tac ctxt k m excludesss;
+fun mk_primcorec_disc_tac ctxt fun_defs corec_disc k m excludesss =
+  prelude_tac ctxt fun_defs corec_disc THEN cases_tac ctxt k m excludesss;
 
 fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss
     distinct_discs =
@@ -129,9 +129,9 @@
      resolve_tac ctxt
       (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' assume_tac ctxt));
 
-fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_ident0s map_comps fun_sel k
-    m excludesss =
-  prelude_tac ctxt defs (fun_sel RS trans) THEN
+fun mk_primcorec_sel_tac ctxt fun_defs distincts splits split_asms mapsx map_ident0s map_comps
+    fun_sel k m excludesss =
+  prelude_tac ctxt fun_defs (fun_sel RS trans) THEN
   cases_tac ctxt k m excludesss THEN
   HEADGOAL (REPEAT_DETERM o (rtac ctxt refl ORELSE'
     eresolve_tac ctxt falseEs ORELSE'
diff -r 6b01bff94d87 -r dc8374620332 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Feb 15 12:47:52 2016 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Feb 15 12:48:10 2016 +0100
@@ -469,8 +469,7 @@
 
     val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
 
-    val ((((((((u, exh_y), xss), yss), fs), gs), w), (p, p'))) =
-      no_defs_lthy
+    val (((((((((u, exh_y), xss), yss), fs), gs), w), (p, p'))), _) = no_defs_lthy
       |> add_bindings
       |> yield_singleton (mk_Frees fc_b_name) fcT
       ||>> yield_singleton (mk_Frees "y") fcT (* for compatibility with "datatype_realizer.ML" *)
@@ -479,8 +478,7 @@
       ||>> mk_Frees "f" case_Ts
       ||>> mk_Frees "g" case_Ts
       ||>> yield_singleton (mk_Frees "z") B
-      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT
-      |> fst;
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
 
     val q = Free (fst p', mk_pred1T B);
 
@@ -679,8 +677,7 @@
 
     fun after_qed ([exhaust_thm] :: thmss) lthy =
       let
-        val ((((((((u, u'), (xss, xss')), fs), gs), h), v), p), _) =
-          lthy
+        val ((((((((u, u'), (xss, xss')), fs), gs), h), v), p), _) = lthy
           |> add_bindings
           |> yield_singleton (apfst (op ~~) oo mk_Frees' fc_b_name) fcT
           ||>> mk_Freess' "x" ctr_Tss