tuning

--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Sep 26 16:17:34 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Sep 26 16:25:12 2013 +0200
@@ -314,12 +314,10 @@
 
     val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings;
 
-    fun can_definitely_rely_on_disc k =
-      not (Binding.is_empty (nth raw_disc_bindings' (k - 1)));
+    fun can_definitely_rely_on_disc k = not (Binding.is_empty (nth raw_disc_bindings' (k - 1)));
     fun can_rely_on_disc k =
       can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2));
-    fun should_omit_disc_binding k =
-      n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
+    fun should_omit_disc_binding k = n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
 
     fun is_disc_binding_valid b =
       not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding));
@@ -388,10 +386,9 @@
     fun mk_case_disj xctr xf xs =
       list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr), HOLogic.mk_eq (w, xf)));
 
-    val case_rhs =
-      fold_rev (fold_rev Term.lambda) [fs, [u]]
-        (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $
-           Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss)));
+    val case_rhs = fold_rev (fold_rev Term.lambda) [fs, [u]]
+      (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $
+         Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss)));
 
     val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy
       |> Local_Theory.define ((case_binding, NoSyn), ((Thm.def_binding case_binding, []), case_rhs))

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 26 16:17:34 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 26 16:25:12 2013 +0200
@@ -800,7 +800,7 @@
               |> HOLogic.mk_Trueprop o HOLogic.mk_eq
               |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
               |> curry Logic.list_all (map dest_Free fun_args);
-            val (distincts, _, _, sel_splits, sel_split_asms) = case_thms_of_term lthy [] rhs_term;
+            val (distincts, _, sel_splits, sel_split_asms) = case_thms_of_term lthy [] rhs_term;
           in
             mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_maps
               nested_map_idents nested_map_comps sel_corec k m exclsss

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 26 16:17:34 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 26 16:25:12 2013 +0200
@@ -70,7 +70,7 @@
   val fold_rev_corec_code_rhs: Proof.context -> (term list -> term -> term list -> 'a -> 'a) ->
     typ list -> term -> 'a -> 'a
   val case_thms_of_term: Proof.context -> typ list -> term ->
-    thm list * thm list * thm list * thm list * thm list
+    thm list * thm list * thm list * thm list
 
   val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
     ((term * term list list) list) list -> local_theory ->
@@ -397,8 +397,8 @@
     val (caseT_names, _) = fold_rev_let_if_case ctxt (K (K I)) bound_Ts t ();
     val ctr_sugars = map (the o ctr_sugar_of ctxt) caseT_names;
   in
-    (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #collapses ctr_sugars,
-     maps #sel_splits ctr_sugars, maps #sel_split_asms ctr_sugars)
+    (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #sel_splits ctr_sugars,
+     maps #sel_split_asms ctr_sugars)
   end;
 
 fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;