--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Sat Sep 28 20:24:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Sat Sep 28 22:47:17 2013 +0200
@@ -131,14 +131,15 @@
disc_co_itersss: thm list list list,
sel_co_iterssss: thm list list list list};
-fun of_fp_sugar f (fp_sugar as {index, ...}) = nth (f fp_sugar) index;
+fun of_fp_sugar f (fp_sugar as ({index, ...}: fp_sugar)) = nth (f fp_sugar) index;
fun eq_fp_sugar ({T = T1, fp = fp1, index = index1, fp_res = fp_res1, ...} : fp_sugar,
{T = T2, fp = fp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) =
T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
-fun morph_fp_sugar phi {T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
- ctr_sugars, co_iterss, mapss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss} =
+fun morph_fp_sugar phi ({T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
+ ctr_sugars, co_iterss, mapss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss}
+ : fp_sugar) =
{T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
fp_res = morph_fp_result phi fp_res,
@@ -768,7 +769,7 @@
fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss,
coiters_args_types as [((pgss, crgsss), _), ((phss, cshsss), _)])
dtor_coinduct dtor_injects dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs kss mss ns
- ctr_defss ctr_sugars coiterss coiter_defss export_args lthy =
+ ctr_defss (ctr_sugars : ctr_sugar list) coiterss coiter_defss export_args lthy =
let
fun mk_ctor_dtor_coiter_thm dtor_inject dtor_ctor coiter =
iffD1 OF [dtor_inject, trans OF [coiter, dtor_ctor RS sym]];
@@ -1420,8 +1421,8 @@
|>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list4 o split_list)
o split_list;
- fun mk_simp_thms {injects, distincts, case_thms, ...} un_folds co_recs mapsx rel_injects
- rel_distincts setss =
+ fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) un_folds co_recs
+ mapsx rel_injects rel_distincts setss =
injects @ distincts @ case_thms @ co_recs @ un_folds @ mapsx @ rel_injects @ rel_distincts
@ flat setss;
@@ -1514,7 +1515,7 @@
(unfoldN, unfold_thmss, K coiter_attrs)]
|> massage_multi_notes;
- fun register_nitpick fpT {ctrs, casex, ...} =
+ fun register_nitpick fpT ({ctrs, casex, ...} : ctr_sugar) =
Nitpick_HOL.register_codatatype fpT (fst (dest_Const casex))
(map (dest_Const o mk_ctr As) ctrs)
|> Generic_Target.theory_declaration;
@@ -1544,10 +1545,10 @@
timer; lthy''
end;
-val co_datatypes = define_co_datatypes (K I) (K I) (K I);
+fun co_datatypes x = define_co_datatypes (K I) (K I) (K I) x;
-val co_datatype_cmd =
- define_co_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term;
+fun co_datatype_cmd x =
+ define_co_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term x;
val parse_ctr_arg =
@{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Sat Sep 28 20:24:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Sat Sep 28 22:47:17 2013 +0200
@@ -55,7 +55,7 @@
val nn = length fpTs;
- fun target_ctr_sugar_of_fp_sugar fpT {T, index, ctr_sugars, ...} =
+ fun target_ctr_sugar_of_fp_sugar fpT ({T, index, ctr_sugars, ...} : fp_sugar) =
let
val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
val phi = Morphism.term_morphism (Term.subst_TVars rho);
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Sat Sep 28 20:24:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Sat Sep 28 22:47:17 2013 +0200
@@ -471,7 +471,7 @@
val perm_Cs' = map substCT perm_Cs;
fun offset_of_ctr 0 _ = 0
- | offset_of_ctr n ({ctrs, ...} :: ctr_sugars) =
+ | offset_of_ctr n (({ctrs, ...} : ctr_sugar) :: ctr_sugars) =
length ctrs + offset_of_ctr (n - 1) ctr_sugars;
fun call_of [i] [T] = (if exists_subtype_in Cs T then Indirect_Rec else No_Rec) i
@@ -487,7 +487,7 @@
rec_thm = rec_thm}
end;
- fun mk_ctr_specs index ctr_sugars iter_thmsss =
+ fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) iter_thmsss =
let
val ctrs = #ctrs (nth ctr_sugars index);
val rec_thmss = co_rec_of (nth iter_thmsss index);
@@ -497,7 +497,8 @@
map4 mk_ctr_spec ctrs (k upto k + n - 1) (nth perm_fun_arg_Tssss index) rec_thmss
end;
- fun mk_spec {T, index, ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...} =
+ fun mk_spec ({T, index, ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...}
+ : fp_sugar) =
{recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of (nth iterss index)),
nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
nested_map_comps = map map_comp_of_bnf nested_bnfs,
@@ -579,8 +580,8 @@
sel_corecs = sel_corecs}
end;
- fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss
- sel_coiterssss =
+ fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) p_is q_isss f_isss f_Tsss
+ coiter_thmsss disc_coitersss sel_coiterssss =
let
val ctrs = #ctrs (nth ctr_sugars index);
val discs = #discs (nth ctr_sugars index);
@@ -597,8 +598,8 @@
corec_thms disc_corecs sel_corecss
end;
- fun mk_spec {T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,
- disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...}
+ fun mk_spec ({T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,
+ disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...} : fp_sugar)
p_is q_isss f_isss f_Tsss =
{corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,