1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sat Sep 28 20:24:13 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sat Sep 28 22:47:17 2013 +0200
     1.3 @@ -131,14 +131,15 @@
     1.4     disc_co_itersss: thm list list list,
     1.5     sel_co_iterssss: thm list list list list};
     1.6  
     1.7 -fun of_fp_sugar f (fp_sugar as {index, ...}) = nth (f fp_sugar) index;
     1.8 +fun of_fp_sugar f (fp_sugar as ({index, ...}: fp_sugar)) = nth (f fp_sugar) index;
     1.9  
    1.10  fun eq_fp_sugar ({T = T1, fp = fp1, index = index1, fp_res = fp_res1, ...} : fp_sugar,
    1.11      {T = T2, fp = fp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) =
    1.12    T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
    1.13  
    1.14 -fun morph_fp_sugar phi {T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
    1.15 -    ctr_sugars, co_iterss, mapss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss} =
    1.16 +fun morph_fp_sugar phi ({T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
    1.17 +    ctr_sugars, co_iterss, mapss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss}
    1.18 +    : fp_sugar) =
    1.19    {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
    1.20      nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
    1.21     fp_res = morph_fp_result phi fp_res,
    1.22 @@ -768,7 +769,7 @@
    1.23  fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss,
    1.24        coiters_args_types as [((pgss, crgsss), _), ((phss, cshsss), _)])
    1.25      dtor_coinduct dtor_injects dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs kss mss ns
    1.26 -    ctr_defss ctr_sugars coiterss coiter_defss export_args lthy =
    1.27 +    ctr_defss (ctr_sugars : ctr_sugar list) coiterss coiter_defss export_args lthy =
    1.28    let
    1.29      fun mk_ctor_dtor_coiter_thm dtor_inject dtor_ctor coiter =
    1.30        iffD1 OF [dtor_inject, trans OF [coiter, dtor_ctor RS sym]];
    1.31 @@ -1420,8 +1421,8 @@
    1.32        |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list4 o split_list)
    1.33          o split_list;
    1.34  
    1.35 -    fun mk_simp_thms {injects, distincts, case_thms, ...} un_folds co_recs mapsx rel_injects
    1.36 -        rel_distincts setss =
    1.37 +    fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) un_folds co_recs
    1.38 +        mapsx rel_injects rel_distincts setss =
    1.39        injects @ distincts @ case_thms @ co_recs @ un_folds @ mapsx @ rel_injects @ rel_distincts
    1.40        @ flat setss;
    1.41  
    1.42 @@ -1514,7 +1515,7 @@
    1.43             (unfoldN, unfold_thmss, K coiter_attrs)]
    1.44            |> massage_multi_notes;
    1.45  
    1.46 -        fun register_nitpick fpT {ctrs, casex, ...} =
    1.47 +        fun register_nitpick fpT ({ctrs, casex, ...} : ctr_sugar) =
    1.48            Nitpick_HOL.register_codatatype fpT (fst (dest_Const casex))
    1.49              (map (dest_Const o mk_ctr As) ctrs)
    1.50            |> Generic_Target.theory_declaration;
    1.51 @@ -1544,10 +1545,10 @@
    1.52      timer; lthy''
    1.53    end;
    1.54  
    1.55 -val co_datatypes = define_co_datatypes (K I) (K I) (K I);
    1.56 +fun co_datatypes x = define_co_datatypes (K I) (K I) (K I) x;
    1.57  
    1.58 -val co_datatype_cmd =
    1.59 -  define_co_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term;
    1.60 +fun co_datatype_cmd x =
    1.61 +  define_co_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term x;
    1.62  
    1.63  val parse_ctr_arg =
    1.64    @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Sat Sep 28 20:24:13 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Sat Sep 28 22:47:17 2013 +0200
     2.3 @@ -55,7 +55,7 @@
     2.4  
     2.5        val nn = length fpTs;
     2.6  
     2.7 -      fun target_ctr_sugar_of_fp_sugar fpT {T, index, ctr_sugars, ...} =
     2.8 +      fun target_ctr_sugar_of_fp_sugar fpT ({T, index, ctr_sugars, ...} : fp_sugar) =
     2.9          let
    2.10            val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
    2.11            val phi = Morphism.term_morphism (Term.subst_TVars rho);

     3.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Sat Sep 28 20:24:13 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Sat Sep 28 22:47:17 2013 +0200
     3.3 @@ -471,7 +471,7 @@
     3.4      val perm_Cs' = map substCT perm_Cs;
     3.5  
     3.6      fun offset_of_ctr 0 _ = 0
     3.7 -      | offset_of_ctr n ({ctrs, ...} :: ctr_sugars) =
     3.8 +      | offset_of_ctr n (({ctrs, ...} : ctr_sugar) :: ctr_sugars) =
     3.9          length ctrs + offset_of_ctr (n - 1) ctr_sugars;
    3.10  
    3.11      fun call_of [i] [T] = (if exists_subtype_in Cs T then Indirect_Rec else No_Rec) i
    3.12 @@ -487,7 +487,7 @@
    3.13           rec_thm = rec_thm}
    3.14        end;
    3.15  
    3.16 -    fun mk_ctr_specs index ctr_sugars iter_thmsss =
    3.17 +    fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) iter_thmsss =
    3.18        let
    3.19          val ctrs = #ctrs (nth ctr_sugars index);
    3.20          val rec_thmss = co_rec_of (nth iter_thmsss index);
    3.21 @@ -497,7 +497,8 @@
    3.22          map4 mk_ctr_spec ctrs (k upto k + n - 1) (nth perm_fun_arg_Tssss index) rec_thmss
    3.23        end;
    3.24  
    3.25 -    fun mk_spec {T, index, ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...} =
    3.26 +    fun mk_spec ({T, index, ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...}
    3.27 +      : fp_sugar) =
    3.28        {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of (nth iterss index)),
    3.29         nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
    3.30         nested_map_comps = map map_comp_of_bnf nested_bnfs,
    3.31 @@ -579,8 +580,8 @@
    3.32           sel_corecs = sel_corecs}
    3.33        end;
    3.34  
    3.35 -    fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss
    3.36 -        sel_coiterssss =
    3.37 +    fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) p_is q_isss f_isss f_Tsss
    3.38 +        coiter_thmsss disc_coitersss sel_coiterssss =
    3.39        let
    3.40          val ctrs = #ctrs (nth ctr_sugars index);
    3.41          val discs = #discs (nth ctr_sugars index);
    3.42 @@ -597,8 +598,8 @@
    3.43            corec_thms disc_corecs sel_corecss
    3.44        end;
    3.45  
    3.46 -    fun mk_spec {T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,
    3.47 -          disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...}
    3.48 +    fun mk_spec ({T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,
    3.49 +          disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...} : fp_sugar)
    3.50          p_is q_isss f_isss f_Tsss =
    3.51        {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
    3.52         nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,