1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 10:16:40 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 11:19:05 2013 +0200
     1.3 @@ -13,10 +13,10 @@
     1.4       pre_bnfs: BNF_Def.bnf list,
     1.5       fp_res: BNF_FP_Util.fp_result,
     1.6       ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list,
     1.7 -     xxfolds: term list,
     1.8 -     xxrecs: term list,
     1.9 -     xxfold_thmss: thm list list,
    1.10 -     xxrec_thmss: thm list list};
    1.11 +     un_folds: term list,
    1.12 +     co_recs: term list,
    1.13 +     un_fold_thmss: thm list list,
    1.14 +     co_rec_thmss: thm list list};
    1.15  
    1.16    val fp_sugar_of: local_theory -> string -> fp_sugar option
    1.17  
    1.18 @@ -78,22 +78,22 @@
    1.19     pre_bnfs: bnf list,
    1.20     fp_res: fp_result,
    1.21     ctr_sugars: ctr_sugar list,
    1.22 -   xxfolds: term list,
    1.23 -   xxrecs: term list,
    1.24 -   xxfold_thmss: thm list list,
    1.25 -   xxrec_thmss: thm list list};
    1.26 +   un_folds: term list,
    1.27 +   co_recs: term list,
    1.28 +   un_fold_thmss: thm list list,
    1.29 +   co_rec_thmss: thm list list};
    1.30  
    1.31  fun eq_fp_sugar ({lfp = lfp1, index = index1, fp_res = fp_res1, ...} : fp_sugar,
    1.32      {lfp = lfp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) =
    1.33    lfp1 = lfp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
    1.34  
    1.35 -fun morph_fp_sugar phi {lfp, index, pre_bnfs, fp_res, ctr_sugars, xxfolds, xxrecs, xxfold_thmss,
    1.36 -    xxrec_thmss} =
    1.37 +fun morph_fp_sugar phi {lfp, index, pre_bnfs, fp_res, ctr_sugars, un_folds, co_recs, un_fold_thmss,
    1.38 +    co_rec_thmss} =
    1.39    {lfp = lfp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
    1.40     fp_res = morph_fp_result phi fp_res, ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars,
    1.41 -   xxfolds = map (Morphism.term phi) xxfolds, xxrecs = map (Morphism.term phi) xxrecs,
    1.42 -   xxfold_thmss = map (map (Morphism.thm phi)) xxfold_thmss,
    1.43 -   xxrec_thmss = map (map (Morphism.thm phi)) xxrec_thmss};
    1.44 +   un_folds = map (Morphism.term phi) un_folds, co_recs = map (Morphism.term phi) co_recs,
    1.45 +   un_fold_thmss = map (map (Morphism.thm phi)) un_fold_thmss,
    1.46 +   co_rec_thmss = map (map (Morphism.thm phi)) co_rec_thmss};
    1.47  
    1.48  structure Data = Generic_Data
    1.49  (
    1.50 @@ -109,13 +109,13 @@
    1.51    Local_Theory.declaration {syntax = false, pervasive = true}
    1.52      (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar)));
    1.53  
    1.54 -fun register_fp_sugars lfp pre_bnfs (fp_res as {ctors, ...}) ctr_sugars xxfolds xxrecs xxfold_thmss
    1.55 -    xxrec_thmss lthy =
    1.56 +fun register_fp_sugars lfp pre_bnfs (fp_res as {ctors, ...}) ctr_sugars un_folds co_recs
    1.57 +    un_fold_thmss co_rec_thmss lthy =
    1.58    (0, lthy)
    1.59    |> fold (fn ctor => fn (kk, lthy) => (kk + 1,
    1.60      register_fp_sugar (fp_name_of_ctor ctor) {lfp = lfp, index = kk,
    1.61 -      pre_bnfs = pre_bnfs, fp_res = fp_res, ctr_sugars = ctr_sugars, xxfolds = xxfolds,
    1.62 -      xxrecs = xxrecs, xxfold_thmss = xxfold_thmss, xxrec_thmss = xxrec_thmss} lthy)) ctors
    1.63 +      pre_bnfs = pre_bnfs, fp_res = fp_res, ctr_sugars = ctr_sugars, un_folds = un_folds,
    1.64 +      co_recs = co_recs, un_fold_thmss = un_fold_thmss, co_rec_thmss = co_rec_thmss} lthy)) ctors
    1.65    |> snd;
    1.66  
    1.67  (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *)
    1.68 @@ -1292,9 +1292,9 @@
    1.69          o split_list;
    1.70  
    1.71      val mk_simp_thmss =
    1.72 -      map7 (fn {injects, distincts, case_thms, ...} => fn xxfolds => fn xxrecs =>
    1.73 +      map7 (fn {injects, distincts, case_thms, ...} => fn un_folds => fn co_recs =>
    1.74          fn mapsx => fn rel_injects => fn rel_distincts => fn setss =>
    1.75 -          injects @ distincts @ case_thms @ xxrecs @ xxfolds @ mapsx @ rel_injects
    1.76 +          injects @ distincts @ case_thms @ co_recs @ un_folds @ mapsx @ rel_injects
    1.77            @ rel_distincts @ flat setss);
    1.78  
    1.79      fun derive_and_note_induct_fold_rec_thms_for_types