# HG changeset patch # User blanchet # Date 1369659601 -7200 # Node ID 1b3f907caf614691456a73c020c5627f10c8ae4e # Parent 012679d3a5affcf074eb3ee2f83e0e7f6dd6b8d5 killed dead argument diff -r 012679d3a5af -r 1b3f907caf61 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon May 27 14:00:32 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon May 27 15:00:01 2013 +0200 @@ -45,14 +45,13 @@ (typ list * typ list) list list list val define_fold_rec: (term list list * typ list list * term list list list) * (term list list * typ list list * term list list list) -> (string -> binding) -> typ list -> - typ list -> typ list -> term -> term -> Proof.context -> - (term * term * thm * thm) * Proof.context + typ list -> term -> term -> Proof.context -> (term * term * thm * thm) * Proof.context val define_unfold_corec: term list * term list list * ((term list list * term list list list list * term list list list list) * (typ list * typ list list list * typ list list)) * ((term list list * term list list list list * term list list list list) * (typ list * typ list list list * typ list list)) -> - (string -> binding) -> typ list -> typ list -> typ list -> term -> term -> Proof.context -> + (string -> binding) -> typ list -> typ list -> term -> term -> Proof.context -> (term * term * thm * thm) * Proof.context val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> thm -> thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> @@ -485,7 +484,7 @@ Term.list_comb (dtor_coiter, map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss) end; -fun define_fold_rec (fold_only, rec_only) mk_binding fpTs As Cs ctor_fold ctor_rec lthy0 = +fun define_fold_rec (fold_only, rec_only) mk_binding fpTs Cs ctor_fold ctor_rec lthy0 = let val thy = Proof_Context.theory_of lthy0; @@ -520,7 +519,7 @@ ((foldx, recx, fold_def, rec_def), lthy') end; -fun define_unfold_corec (cs, cpss, unfold_only, corec_only) mk_binding fpTs As Cs dtor_unfold +fun define_unfold_corec (cs, cpss, unfold_only, corec_only) mk_binding fpTs Cs dtor_unfold dtor_corec lthy0 = let val thy = Proof_Context.theory_of lthy0; @@ -555,7 +554,7 @@ val [unfold, corec] = map (mk_co_iter thy false fpT Cs o Morphism.term phi) csts; in ((unfold, corec, unfold_def, corec_def), lthy') - end; + end ; fun derive_induct_fold_rec_thms_for_types pre_bnfs ctor_folds ctor_recs ctor_induct ctor_fold_thms ctor_rec_thms nesting_bnfs nested_bnfs fpTs Cs ctrss ctr_defss folds recs fold_defs rec_defs @@ -1330,8 +1329,7 @@ (wrap_ctrs #> derive_maps_sets_rels ##>> (if lfp then define_fold_rec (the fold_rec_args_types) - else define_unfold_corec (the unfold_corec_args_types)) - mk_binding fpTs As Cs fp_fold fp_rec + else define_unfold_corec (the unfold_corec_args_types)) mk_binding fpTs Cs fp_fold fp_rec #> massage_res, lthy') end;