# HG changeset patch
# User traytel
# Date 1376040389 -7200
# Node ID ec63c82551aefce14de0b957ed49b1a393b90c5d
# Parent  d1bcb4479a2f8fe4679453cf29b86428bd8efea4
tuned

diff -r d1bcb4479a2f -r ec63c82551ae src/HOL/BNF/Tools/bnf_comp.ML
--- 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);
 
diff -r d1bcb4479a2f -r ec63c82551ae src/HOL/BNF/Tools/bnf_def.ML
--- 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
diff -r d1bcb4479a2f -r ec63c82551ae src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- 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
diff -r d1bcb4479a2f -r ec63c82551ae src/HOL/BNF/Tools/bnf_fp_util.ML
--- 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;
 
diff -r d1bcb4479a2f -r ec63c82551ae src/HOL/BNF/Tools/bnf_gfp.ML
--- 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;
diff -r d1bcb4479a2f -r ec63c82551ae src/HOL/BNF/Tools/bnf_lfp.ML
--- 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);