--- a/src/HOL/BNF/Tools/bnf_comp.ML Thu Aug 08 20:43:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Fri Aug 09 11:26:29 2013 +0200
@@ -98,7 +98,7 @@
val Bss_repl = replicate olive Bs;
val ((((fs', Qs'), Asets), xs), _(*names_lthy*)) = lthy
- |> apfst snd o mk_Frees' "f" (map2 (curry (op -->)) As Bs)
+ |> apfst snd o mk_Frees' "f" (map2 (curry op -->) As Bs)
||>> apfst snd o mk_Frees' "Q" (map2 mk_pred2T As Bs)
||>> mk_Frees "A" (map HOLogic.mk_setT As)
||>> mk_Frees "x" As;
@@ -378,7 +378,7 @@
(*%f1 ... fn. bnf.map*)
val mapx =
- fold_rev Term.absdummy (map2 (curry (op -->)) newAs newBs) (mk_map_of_bnf Ds As Bs bnf);
+ fold_rev Term.absdummy (map2 (curry op -->) newAs newBs) (mk_map_of_bnf Ds As Bs bnf);
(*%Q1 ... Qn. bnf.rel*)
val rel = fold_rev Term.absdummy (map2 mk_pred2T newAs newBs) (mk_rel_of_bnf Ds As Bs bnf);
--- a/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 08 20:43:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Fri Aug 09 11:26:29 2013 +0200
@@ -760,9 +760,9 @@
val (((((((((((((((((((((((((fs, gs), hs), x), y), (z, z')), zs), ys), As),
As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss),
transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy
- |> mk_Frees "f" (map2 (curry (op -->)) As' Bs')
- ||>> mk_Frees "g" (map2 (curry (op -->)) Bs' Cs)
- ||>> mk_Frees "h" (map2 (curry (op -->)) As' Ts)
+ |> mk_Frees "f" (map2 (curry op -->) As' Bs')
+ ||>> mk_Frees "g" (map2 (curry op -->) Bs' Cs)
+ ||>> mk_Frees "h" (map2 (curry op -->) As' Ts)
||>> yield_singleton (mk_Frees "x") CA'
||>> yield_singleton (mk_Frees "y") CB'
||>> yield_singleton (apfst (op ~~) oo mk_Frees' "z") CRs'
@@ -773,12 +773,12 @@
||>> mk_Frees "A" (map HOLogic.mk_setT domTs)
||>> mk_Frees "B1" (map HOLogic.mk_setT B1Ts)
||>> mk_Frees "B2" (map HOLogic.mk_setT B2Ts)
- ||>> mk_Frees "f1" (map2 (curry (op -->)) B1Ts ranTs)
- ||>> mk_Frees "f2" (map2 (curry (op -->)) B2Ts ranTs)
- ||>> mk_Frees "e1" (map2 (curry (op -->)) B1Ts ranTs')
- ||>> mk_Frees "e2" (map2 (curry (op -->)) B2Ts ranTs'')
- ||>> mk_Frees "p1" (map2 (curry (op -->)) domTs B1Ts)
- ||>> mk_Frees "p2" (map2 (curry (op -->)) domTs B2Ts)
+ ||>> mk_Frees "f1" (map2 (curry op -->) B1Ts ranTs)
+ ||>> mk_Frees "f2" (map2 (curry op -->) B2Ts ranTs)
+ ||>> mk_Frees "e1" (map2 (curry op -->) B1Ts ranTs')
+ ||>> mk_Frees "e2" (map2 (curry op -->) B2Ts ranTs'')
+ ||>> mk_Frees "p1" (map2 (curry op -->) domTs B1Ts)
+ ||>> mk_Frees "p2" (map2 (curry op -->) domTs B2Ts)
||>> mk_Frees "b" As'
||>> mk_Frees' "R" pred2RTs
||>> mk_Frees "R" pred2RTs
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 08 20:43:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Aug 09 11:26:29 2013 +0200
@@ -328,7 +328,7 @@
fun nesty_bnfs ctxt ctr_Tsss Us =
map_filter (bnf_of ctxt) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_Tsss []);
-fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p;
+fun indexify proj xs f p = f (find_index (curry op = (proj p)) xs) p;
fun mk_iter_fun_arg_types0 n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
@@ -356,7 +356,7 @@
dest_sumTN_balanced n o domain_type o co_rec_of) ns mss ctor_iter_fun_Tss;
val z_Tsss' = map (map flat_rec_arg_args) z_Tssss;
- val h_Tss = map2 (map2 (curry (op --->))) z_Tsss' Css;
+ val h_Tss = map2 (map2 (curry op --->)) z_Tsss' Css;
val hss = map2 (map2 retype_free) h_Tss gss;
val zssss_hd = map2 (map2 (map2 (retype_free o hd))) z_Tssss ysss;
@@ -377,7 +377,7 @@
val f_sum_prod_Ts = map range_type fun_Ts;
val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts;
val f_Tsss = map2 (map2 dest_tupleT o repair_arity) mss f_prod_Tss;
- val f_Tssss = map2 (fn C => map (map (map (curry (op -->) C) o unzip_corecT Cs))) Cs f_Tsss;
+ val f_Tssss = map2 (fn C => map (map (map (curry op --> C) o unzip_corecT Cs))) Cs f_Tsss;
val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss;
in
(q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts)
@@ -498,7 +498,7 @@
fun generate_iter suf (f_Tss, _, fss, xssss) ctor_iter =
let
- val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
+ val res_T = fold_rev (curry op --->) f_Tss fpT_to_C;
val b = mk_binding suf;
val spec =
mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of b, res_T)),
@@ -517,7 +517,7 @@
fun generate_coiter suf ((pfss, cqfsss), (f_sum_prod_Ts, pf_Tss)) dtor_coiter =
let
- val res_T = fold_rev (curry (op --->)) pf_Tss C_to_fpT;
+ val res_T = fold_rev (curry op --->) pf_Tss C_to_fpT;
val b = mk_binding suf;
val spec =
mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of b, res_T)),
@@ -566,7 +566,7 @@
val lives = lives_of_bnf bnf;
val sets = sets_of_bnf bnf;
fun mk_set U =
- (case find_index (curry (op =) U) lives of
+ (case find_index (curry op = U) lives of
~1 => Term.dummy
| i => nth sets i);
in
@@ -583,7 +583,7 @@
end;
fun mk_raw_prem_prems _ (x as Free (_, Type _)) (X as TFree _) =
- [([], (find_index (curry (op =) X) Xs + 1, x))]
+ [([], (find_index (curry op = X) Xs + 1, x))]
| mk_raw_prem_prems names_lthy (x as Free (s, Type (T_name, Ts0))) (Type (_, Xs_Ts0)) =
(case AList.lookup (op =) setss_nested T_name of
NONE => []
@@ -623,7 +623,7 @@
val goal =
Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
- HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) ps us)));
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry op $) ps us)));
val kksss = map (map (map (fst o snd) o #2)) raw_premss;
@@ -740,7 +740,7 @@
(* TODO: generalize (cf. "build_map") *)
fun build_rel rs' T =
- (case find_index (curry (op =) T) fpTs of
+ (case find_index (curry op = T) fpTs of
~1 =>
if exists_subtype_in fpTs T then
let
@@ -883,8 +883,8 @@
map2 (map2 prove) corec_goalss corec_tacss
|> map (map (unfold_thms lthy @{thms sum_case_if}));
- val unfold_safesss = map2 (map2 (map2 (curry (op =)))) crgsss' crgsss;
- val corec_safesss = map2 (map2 (map2 (curry (op =)))) cshsss' cshsss;
+ val unfold_safesss = map2 (map2 (map2 (curry op =))) crgsss' crgsss;
+ val corec_safesss = map2 (map2 (map2 (curry op =))) cshsss' cshsss;
val filter_safesss =
map2 (map_filter (fn (safes, thm) => if forall I safes then SOME thm else NONE) oo
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Aug 08 20:43:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Fri Aug 09 11:26:29 2013 +0200
@@ -471,7 +471,7 @@
fun mk_sumEN_tupled_balanced ms =
let val n = length ms in
- if forall (curry (op =) 1) ms then mk_sumEN_balanced n
+ if forall (curry op = 1) ms then mk_sumEN_balanced n
else mk_sumEN_balanced' n (map mk_tupled_allIN ms)
end;
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 08 20:43:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Fri Aug 09 11:26:29 2013 +0200
@@ -1658,8 +1658,8 @@
mk_map_of_bnf Ds (passiveAs @ prodTs) (passiveAs @ Ts)) Dss bnfs;
val fstsTs = map fst_const prodTs;
val sndsTs = map snd_const prodTs;
- val dtorTs = map2 (curry (op -->)) Ts FTs;
- val ctorTs = map2 (curry (op -->)) FTs Ts;
+ val dtorTs = map2 (curry op -->) Ts FTs;
+ val ctorTs = map2 (curry op -->) FTs Ts;
val unfold_fTs = map2 (curry op -->) activeAs Ts;
val corec_sTs = map (Term.typ_subst_atomic (activeBs ~~ Ts)) sum_sTs;
val corec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls;
@@ -1765,7 +1765,7 @@
fun mk_unfolds passives actives =
map3 (fn name => fn T => fn active =>
Const (name, Library.foldr (op -->)
- (map2 (curry (op -->)) actives (mk_FTs (passives @ actives)), active --> T)))
+ (map2 (curry op -->) actives (mk_FTs (passives @ actives)), active --> T)))
unfold_names (mk_Ts passives) actives;
fun mk_unfold Ts ss i = Term.list_comb (Const (nth unfold_names (i - 1), Library.foldr (op -->)
(map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
@@ -2410,7 +2410,7 @@
val thePullTs = passiveXs @ map2 (curry HOLogic.mk_prodT) Ts Ts';
val thePull_ins = map2 (mk_in (AXs @ thePulls)) (mk_setss thePullTs) (mk_FTs thePullTs);
val pickFs = map5 mk_pickWP thePull_ins pfst_Fmaps psnd_Fmaps
- (map2 (curry (op $)) dtors Jzs) (map2 (curry (op $)) dtor's Jz's);
+ (map2 (curry op $) dtors Jzs) (map2 (curry op $) dtor's Jz's);
val pickF_ss = map3 (fn pickF => fn z => fn z' =>
HOLogic.mk_split (Term.absfree z (Term.absfree z' pickF))) pickFs Jzs' Jz's';
val picks = map (mk_unfold XTs pickF_ss) ks;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 08 20:43:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Fri Aug 09 11:26:29 2013 +0200
@@ -75,17 +75,17 @@
val BTs = map HOLogic.mk_setT activeAs;
val B'Ts = map HOLogic.mk_setT activeBs;
val B''Ts = map HOLogic.mk_setT activeCs;
- val sTs = map2 (curry (op -->)) FTsAs activeAs;
- val s'Ts = map2 (curry (op -->)) FTsBs activeBs;
- val s''Ts = map2 (curry (op -->)) FTsCs activeCs;
- val fTs = map2 (curry (op -->)) activeAs activeBs;
- val inv_fTs = map2 (curry (op -->)) activeBs activeAs;
- val self_fTs = map2 (curry (op -->)) activeAs activeAs;
- val gTs = map2 (curry (op -->)) activeBs activeCs;
- val all_gTs = map2 (curry (op -->)) allBs allCs';
+ val sTs = map2 (curry op -->) FTsAs activeAs;
+ val s'Ts = map2 (curry op -->) FTsBs activeBs;
+ val s''Ts = map2 (curry op -->) FTsCs activeCs;
+ val fTs = map2 (curry op -->) activeAs activeBs;
+ val inv_fTs = map2 (curry op -->) activeBs activeAs;
+ val self_fTs = map2 (curry op -->) activeAs activeAs;
+ val gTs = map2 (curry op -->) activeBs activeCs;
+ val all_gTs = map2 (curry op -->) allBs allCs';
val prodBsAs = map2 (curry HOLogic.mk_prodT) activeBs activeAs;
val prodFTs = mk_FTs (passiveAs @ prodBsAs);
- val prod_sTs = map2 (curry (op -->)) prodFTs activeAs;
+ val prod_sTs = map2 (curry op -->) prodFTs activeAs;
(* terms *)
val mapsAsAs = map4 mk_map_of_bnf Dss Ass Ass bnfs;
@@ -1094,7 +1094,7 @@
fun mk_folds passives actives =
map3 (fn name => fn T => fn active =>
Const (name, Library.foldr (op -->)
- (map2 (curry (op -->)) (mk_FTs (passives @ actives)) actives, T --> active)))
+ (map2 (curry op -->) (mk_FTs (passives @ actives)) actives, T --> active)))
fold_names (mk_Ts passives) actives;
fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->)
(map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);