# HG changeset patch # User wenzelm # Date 1380401237 -7200 # Node ID 61250526325725ef5b25c65e342ae01638fae6c0 # Parent 78bbe75c8437ff8bc474dde7993714ada998af27 make SML/NJ more happy; diff -r 78bbe75c8437 -r 612505263257 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- 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 ")"} || diff -r 78bbe75c8437 -r 612505263257 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML --- 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); diff -r 78bbe75c8437 -r 612505263257 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML --- 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,