# HG changeset patch
# User blanchet
# Date 1392190556 -3600
# Node ID 1e8dd9cd320bf87ad0589efb6fb6970d01ac7a92
# Parent  5c8e91f884af413c5dcfb6eca535307c6b25cf8b
tuning

diff -r 5c8e91f884af -r 1e8dd9cd320b src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -340,22 +340,8 @@
 fun fold_rev_corec_code_rhs ctxt f =
   fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb);
 
-fun case_thms_of_term ctxt bound_Ts t =
-  let
-    fun ctr_sugar_of_case c s =
-      (case ctr_sugar_of ctxt s of
-        SOME (ctr_sugar as {casex = Const (c', _), sel_splits = _ :: _, ...}) =>
-        if c' = c then SOME ctr_sugar else NONE
-      | _ => NONE);
-    fun add_ctr_sugar (s, Type (@{type_name fun}, [_, T])) =
-        binder_types T
-        |> map_filter (try (fst o dest_Type))
-        |> distinct (op =)
-        |> map_filter (ctr_sugar_of_case s)
-      | add_ctr_sugar _ = [];
-
-    val ctr_sugars = maps add_ctr_sugar (Term.add_consts t []);
-  in
+fun case_thms_of_term ctxt t =
+  let val ctr_sugars = map_filter (Ctr_Sugar.ctr_sugar_of_case ctxt o fst) (Term.add_consts t []) in
     (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #disc_exhausts ctr_sugars,
      maps #sel_splits ctr_sugars, maps #sel_split_asms ctr_sugars)
   end;
@@ -1020,12 +1006,12 @@
         de_facto_exhaustives disc_eqnss
       |> list_all_fun_args []
     val nchotomy_taut_thmss =
-      map6 (fn tac_opt => fn {disc_exhausts = res_disc_exhausts, ...} => fn arg_Ts =>
+      map5 (fn tac_opt => fn {disc_exhausts = res_disc_exhausts, ...} =>
           fn {code_rhs_opt, ...} :: _ => fn [] => K []
             | [goal] => fn true =>
               let
                 val (_, _, arg_disc_exhausts, _, _) =
-                  case_thms_of_term lthy arg_Ts (the_default Term.dummy code_rhs_opt);
+                  case_thms_of_term lthy (the_default Term.dummy code_rhs_opt);
               in
                 [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
                    mk_primcorec_nchotomy_tac ctxt (res_disc_exhausts @ arg_disc_exhausts))
@@ -1035,7 +1021,7 @@
               (case tac_opt of
                 SOME tac => [Goal.prove_sorry lthy [] [] goal tac |> Thm.close_derivation]
               | NONE => []))
-        tac_opts corec_specs arg_Tss disc_eqnss nchotomy_goalss syntactic_exhaustives;
+        tac_opts corec_specs disc_eqnss nchotomy_goalss syntactic_exhaustives;
 
     val syntactic_exhaustives =
       map (fn disc_eqns => forall (null o #prems orf is_some o #code_rhs_opt) disc_eqns
@@ -1132,7 +1118,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 excludesss
@@ -1258,7 +1244,7 @@
                       |> pairself (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
                         #> curry Logic.list_all (map dest_Free fun_args));
                     val (distincts, discIs, _, sel_splits, sel_split_asms) =
-                      case_thms_of_term lthy bound_Ts raw_rhs;
+                      case_thms_of_term lthy raw_rhs;
 
                     val raw_code_thm = mk_primcorec_raw_code_tac lthy distincts discIs sel_splits
                         sel_split_asms ms ctr_thms