1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 30 16:04:50 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 30 16:18:21 2013 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4       index: int,
     1.5       pre_bnfs: BNF_Def.bnf list,
     1.6       fp_res: BNF_FP.fp_result,
     1.7 -     ctr_sugar: BNF_Ctr_Sugar.ctr_sugar};
     1.8 +     ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list};
     1.9  
    1.10    val fp_sugar_of: Proof.context -> string -> fp_sugar option
    1.11  
    1.12 @@ -64,15 +64,15 @@
    1.13     index: int,
    1.14     pre_bnfs: bnf list,
    1.15     fp_res: fp_result,
    1.16 -   ctr_sugar: ctr_sugar};
    1.17 +   ctr_sugars: ctr_sugar list};
    1.18  
    1.19  fun eq_fp_sugar ({lfp = lfp1, index = index1, fp_res = fp_res1, ...} : fp_sugar,
    1.20      {lfp = lfp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) =
    1.21    lfp1 = lfp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
    1.22  
    1.23 -fun morph_fp_sugar phi {lfp, index, pre_bnfs, fp_res, ctr_sugar} =
    1.24 +fun morph_fp_sugar phi {lfp, index, pre_bnfs, fp_res, ctr_sugars} =
    1.25    {lfp = lfp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
    1.26 -   fp_res = morph_fp_result phi fp_res, ctr_sugar = morph_ctr_sugar phi ctr_sugar};
    1.27 +   fp_res = morph_fp_result phi fp_res, ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars};
    1.28  
    1.29  structure Data = Generic_Data
    1.30  (
    1.31 @@ -89,10 +89,10 @@
    1.32      (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar)));
    1.33  
    1.34  fun register_fp_sugars lfp pre_bnfs (fp_res as {ctors, ...}) ctr_sugars lthy =
    1.35 -  ((1, ctors), lthy)
    1.36 -  |> fold (fn ctr_sugar => fn ((kk, ctor :: ctors), lthy) =>
    1.37 -    ((kk + 1, ctors), register_fp_sugar (fp_name_of_ctor ctor) {lfp = lfp, index = kk,
    1.38 -       pre_bnfs = pre_bnfs, fp_res = fp_res, ctr_sugar = ctr_sugar} lthy)) ctr_sugars
    1.39 +  (1, lthy)
    1.40 +  |> fold (fn ctor => fn (kk, lthy) => (kk + 1,
    1.41 +    register_fp_sugar (fp_name_of_ctor ctor) {lfp = lfp, index = kk,
    1.42 +      pre_bnfs = pre_bnfs, fp_res = fp_res, ctr_sugars = ctr_sugars} lthy)) ctors
    1.43    |> snd;
    1.44  
    1.45  (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *)