--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu May 02 18:25:44 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu May 02 18:34:36 2013 +0200
@@ -50,16 +50,16 @@
* (thm list list * thm list list * Args.src list)
* (thm list list * thm list list * Args.src list)
- val co_datatypes: bool -> (mixfix list -> binding list -> binding list -> binding list ->
- binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
+ val co_datatypes: bool -> (mixfix list -> binding list -> binding list -> binding list list ->
+ binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
local_theory -> BNF_FP_Util.fp_result * local_theory) ->
(bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
((((binding * binding) * (binding * typ) list) * (binding * term) list) *
mixfix) list) list ->
local_theory -> local_theory
- val parse_co_datatype_cmd: bool -> (mixfix list -> binding list -> binding list -> binding list ->
- binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
- local_theory -> BNF_FP_Util.fp_result * local_theory) ->
+ val parse_co_datatype_cmd: bool -> (mixfix list -> binding list -> binding list ->
+ binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
+ BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
(local_theory -> local_theory) parser
end;
@@ -912,8 +912,8 @@
folds = fp_folds0, recs = fp_recs0, induct = fp_induct, strong_induct = fp_strong_induct,
dtor_ctors, ctor_dtors, ctor_injects, map_thms = fp_map_thms, set_thmss = fp_set_thmss,
rel_thms = fp_rel_thms, fold_thms = fp_fold_thms, rec_thms = fp_rec_thms, ...}, lthy)) =
- fp_bnf construct_fp fp_bs mixfixes map_bs rel_bs set_bss (map dest_TFree unsorted_As) fp_eqs
- no_defs_lthy0;
+ fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs mixfixes map_bs rel_bs set_bss
+ (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
val timer = time (Timer.startRealTimer ());
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu May 02 18:25:44 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Thu May 02 18:34:36 2013 +0200
@@ -165,8 +165,8 @@
val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
- val fp_bnf: (mixfix list -> binding list -> binding list -> binding list -> binding list list ->
- (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> 'a) ->
+ val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
+ BNF_Def.bnf list -> local_theory -> 'a) ->
binding list -> mixfix list -> binding list -> binding list -> binding list list ->
(string * sort) list -> ((string * sort) * typ) list -> local_theory -> BNF_Def.bnf list * 'a
end;
@@ -491,7 +491,7 @@
val timer = time (timer "Normalization & sealing of BNFs");
- val res = construct_fp resBs (map TFree resDs, deadss) pre_bnfs lthy'';
+ val res = construct_fp bs resBs (map TFree resDs, deadss) pre_bnfs lthy'';
val timer = time (timer "FP construction in total");
in
@@ -508,8 +508,7 @@
(fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss
(empty_unfolds, lthy));
in
- mk_fp_bnf timer (construct_fp mixfixes bs map_bs rel_bs set_bss) resBs bs sort lhss bnfs Dss Ass
- unfold_set lthy'
+ mk_fp_bnf timer construct_fp resBs bs sort lhss bnfs Dss Ass unfold_set lthy'
end;
end;
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu May 02 18:25:44 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu May 02 18:34:36 2013 +0200
@@ -9,8 +9,8 @@
signature BNF_GFP =
sig
- val construct_gfp: mixfix list -> binding list -> binding list -> binding list ->
- binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
+ val construct_gfp: mixfix list -> binding list -> binding list -> binding list list ->
+ binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
local_theory -> BNF_FP_Util.fp_result * local_theory
end;
@@ -55,7 +55,7 @@
((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
(*all BNFs have the same lives*)
-fun construct_gfp mixfixes bs map_bs rel_bs set_bss resBs (resDs, Dss) bnfs lthy =
+fun construct_gfp mixfixes map_bs rel_bs set_bss bs resBs (resDs, Dss) bnfs lthy =
let
val timer = time (Timer.startRealTimer ());
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu May 02 18:25:44 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu May 02 18:34:36 2013 +0200
@@ -8,8 +8,8 @@
signature BNF_LFP =
sig
- val construct_lfp: mixfix list -> binding list -> binding list -> binding list ->
- binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
+ val construct_lfp: mixfix list -> binding list -> binding list -> binding list list ->
+ binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
local_theory -> BNF_FP_Util.fp_result * local_theory
end;
@@ -26,7 +26,7 @@
open BNF_LFP_Tactics
(*all BNFs have the same lives*)
-fun construct_lfp mixfixes bs map_bs rel_bs set_bss resBs (resDs, Dss) bnfs lthy =
+fun construct_lfp mixfixes map_bs rel_bs set_bss bs resBs (resDs, Dss) bnfs lthy =
let
val timer = time (Timer.startRealTimer ());