1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Oct 01 14:05:25 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Oct 01 14:13:24 2013 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature BNF_FP_N2M_SUGAR =
     1.6  sig
     1.7 -  val mutualize_fp_sugars: bool -> bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
     1.8 +  val mutualize_fp_sugars: bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
     1.9      (term -> int list) -> term list list list list -> BNF_FP_Def_Sugar.fp_sugar list ->
    1.10      local_theory ->
    1.11      (BNF_FP_Def_Sugar.fp_sugar list
    1.12 @@ -15,8 +15,8 @@
    1.13      * local_theory
    1.14    val pad_and_indexify_calls: BNF_FP_Def_Sugar.fp_sugar list -> int ->
    1.15      (term * term list list) list list -> term list list list list
    1.16 -  val nested_to_mutual_fps: bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
    1.17 -    (term -> int list) -> ((term * term list list) list) list -> local_theory ->
    1.18 +  val nested_to_mutual_fps: BNF_FP_Util.fp_kind -> binding list -> typ list -> (term -> int list) ->
    1.19 +    (term * term list list) list list -> local_theory ->
    1.20      (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
    1.21       * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
    1.22      * local_theory
    1.23 @@ -37,9 +37,7 @@
    1.24  (* TODO: test with sort constraints on As *)
    1.25  (* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables
    1.26     as deads? *)
    1.27 -fun mutualize_fp_sugars lose_co_rec mutualize fp bs fpTs get_indices callssss fp_sugars0
    1.28 -    no_defs_lthy0 =
    1.29 -  (* TODO: Also check whether there's any lost recursion? *)
    1.30 +fun mutualize_fp_sugars mutualize fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 =
    1.31    if mutualize orelse has_duplicates (op =) fpTs then
    1.32      let
    1.33        val thy = Proof_Context.theory_of no_defs_lthy0;
    1.34 @@ -79,11 +77,6 @@
    1.35          |> mk_TFrees nn
    1.36          ||>> variant_tfrees fp_b_names;
    1.37  
    1.38 -      (* If "lose_co_rec" is "true", the function "null" on "'a list" gives rise to
    1.39 -           'list = unit + 'a list
    1.40 -         instead of
    1.41 -           'list = unit + 'list
    1.42 -         resulting in a simpler (co)induction rule and (co)recursor. *)
    1.43        fun freeze_fp_default (T as Type (s, Ts)) =
    1.44            (case find_index (curry (op =) T) fpTs of
    1.45              ~1 => Type (s, map freeze_fp_default Ts)
    1.46 @@ -100,7 +93,7 @@
    1.47              [] =>
    1.48              (case union (op = o pairself fst)
    1.49                  (maps (fn call => map (rpair call) (get_indices_checked call)) calls) [] of
    1.50 -              [] => T |> not lose_co_rec ? freeze_fp_default
    1.51 +              [] => freeze_fp_default T
    1.52              | [(kk, _)] => nth Xs kk
    1.53              | (_, call1) :: (_, call2) :: _ => incompatible_calls call1 call2)
    1.54            | callss =>
    1.55 @@ -201,7 +194,7 @@
    1.56  
    1.57  fun pad_and_indexify_calls fp_sugars0 = map2 indexify_callsss fp_sugars0 oo pad_list [];
    1.58  
    1.59 -fun nested_to_mutual_fps lose_co_rec fp actual_bs actual_Ts get_indices actual_callssss0 lthy =
    1.60 +fun nested_to_mutual_fps fp actual_bs actual_Ts get_indices actual_callssss0 lthy =
    1.61    let
    1.62      val qsoty = quote o Syntax.string_of_typ lthy;
    1.63      val qsotys = space_implode " or " o map qsoty;
    1.64 @@ -264,7 +257,7 @@
    1.65      val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
    1.66  
    1.67      val ((perm_fp_sugars, fp_sugar_thms), lthy) =
    1.68 -      mutualize_fp_sugars lose_co_rec mutualize fp perm_bs perm_Ts get_perm_indices perm_callssss
    1.69 +      mutualize_fp_sugars mutualize fp perm_bs perm_Ts get_perm_indices perm_callssss
    1.70          perm_fp_sugars0 lthy;
    1.71  
    1.72      val fp_sugars = unpermute perm_fp_sugars;