# HG changeset patch
# User blanchet
# Date 1380629604 -7200
# Node ID f138452e8265704b771a7dbe459ddab11d2ab110
# Parent  b15cfc2864dede0d8b84eb5f11f183d6bad778bc
got rid of dead feature

diff -r b15cfc2864de -r f138452e8265 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Oct 01 14:05:25 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Oct 01 14:13:24 2013 +0200
@@ -7,7 +7,7 @@
 
 signature BNF_FP_N2M_SUGAR =
 sig
-  val mutualize_fp_sugars: bool -> bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
+  val mutualize_fp_sugars: bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
     (term -> int list) -> term list list list list -> BNF_FP_Def_Sugar.fp_sugar list ->
     local_theory ->
     (BNF_FP_Def_Sugar.fp_sugar list
@@ -15,8 +15,8 @@
     * local_theory
   val pad_and_indexify_calls: BNF_FP_Def_Sugar.fp_sugar list -> int ->
     (term * term list list) list list -> term list list list list
-  val nested_to_mutual_fps: bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
-    (term -> int list) -> ((term * term list list) list) list -> local_theory ->
+  val nested_to_mutual_fps: BNF_FP_Util.fp_kind -> binding list -> typ list -> (term -> int list) ->
+    (term * term list list) list list -> local_theory ->
     (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
      * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
     * local_theory
@@ -37,9 +37,7 @@
 (* TODO: test with sort constraints on As *)
 (* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables
    as deads? *)
-fun mutualize_fp_sugars lose_co_rec mutualize fp bs fpTs get_indices callssss fp_sugars0
-    no_defs_lthy0 =
-  (* TODO: Also check whether there's any lost recursion? *)
+fun mutualize_fp_sugars mutualize fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 =
   if mutualize orelse has_duplicates (op =) fpTs then
     let
       val thy = Proof_Context.theory_of no_defs_lthy0;
@@ -79,11 +77,6 @@
         |> mk_TFrees nn
         ||>> variant_tfrees fp_b_names;
 
-      (* If "lose_co_rec" is "true", the function "null" on "'a list" gives rise to
-           'list = unit + 'a list
-         instead of
-           'list = unit + 'list
-         resulting in a simpler (co)induction rule and (co)recursor. *)
       fun freeze_fp_default (T as Type (s, Ts)) =
           (case find_index (curry (op =) T) fpTs of
             ~1 => Type (s, map freeze_fp_default Ts)
@@ -100,7 +93,7 @@
             [] =>
             (case union (op = o pairself fst)
                 (maps (fn call => map (rpair call) (get_indices_checked call)) calls) [] of
-              [] => T |> not lose_co_rec ? freeze_fp_default
+              [] => freeze_fp_default T
             | [(kk, _)] => nth Xs kk
             | (_, call1) :: (_, call2) :: _ => incompatible_calls call1 call2)
           | callss =>
@@ -201,7 +194,7 @@
 
 fun pad_and_indexify_calls fp_sugars0 = map2 indexify_callsss fp_sugars0 oo pad_list [];
 
-fun nested_to_mutual_fps lose_co_rec fp actual_bs actual_Ts get_indices actual_callssss0 lthy =
+fun nested_to_mutual_fps fp actual_bs actual_Ts get_indices actual_callssss0 lthy =
   let
     val qsoty = quote o Syntax.string_of_typ lthy;
     val qsotys = space_implode " or " o map qsoty;
@@ -264,7 +257,7 @@
     val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
 
     val ((perm_fp_sugars, fp_sugar_thms), lthy) =
-      mutualize_fp_sugars lose_co_rec mutualize fp perm_bs perm_Ts get_perm_indices perm_callssss
+      mutualize_fp_sugars mutualize fp perm_bs perm_Ts get_perm_indices perm_callssss
         perm_fp_sugars0 lthy;
 
     val fp_sugars = unpermute perm_fp_sugars;
diff -r b15cfc2864de -r f138452e8265 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Tue Oct 01 14:05:25 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Tue Oct 01 14:13:24 2013 +0200
@@ -422,8 +422,6 @@
       | NONE => [])
   | map_thms_of_typ _ _ = [];
 
-val lose_co_rec = false (*FIXME: try true?*);
-
 fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
   let
     val thy = Proof_Context.theory_of lthy;
@@ -431,7 +429,7 @@
     val ((missing_arg_Ts, perm0_kks,
           fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = ctor_iters1 :: _, ...},
             co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)), lthy') =
-      nested_to_mutual_fps lose_co_rec Least_FP bs arg_Ts get_indices callssss0 lthy;
+      nested_to_mutual_fps Least_FP bs arg_Ts get_indices callssss0 lthy;
 
     val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
 
@@ -515,7 +513,7 @@
     val ((missing_res_Ts, perm0_kks,
           fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
             co_inducts = coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy') =
-      nested_to_mutual_fps lose_co_rec Greatest_FP bs res_Ts get_indices callssss0 lthy;
+      nested_to_mutual_fps Greatest_FP bs res_Ts get_indices callssss0 lthy;
 
     val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
 
diff -r b15cfc2864de -r f138452e8265 src/HOL/BNF/Tools/bnf_lfp_compat.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Tue Oct 01 14:05:25 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Tue Oct 01 14:13:24 2013 +0200
@@ -95,8 +95,7 @@
     val has_nested = nn > nn_fp;
 
     val ((fp_sugars, (lfp_sugar_thms, _)), lthy) =
-      mutualize_fp_sugars false has_nested Least_FP compat_bs Ts get_indices callssss fp_sugars0
-        lthy;
+      mutualize_fp_sugars has_nested Least_FP compat_bs Ts get_indices callssss fp_sugars0 lthy;
 
     val {ctr_sugars, co_inducts = [induct], co_iterss, co_iter_thmsss = iter_thmsss, ...} :: _ =
       fp_sugars;