# HG changeset patch
# User wenzelm
# Date 1417017343 -3600
# Node ID 5b649fb2f2e10046a11607a6c29353e6015f3c3f
# Parent  cbe9563c03d1d5d00493c489df51809d8d0dd43d
added ML antiquotation @{apply n} or @{apply n(k)};

diff -r cbe9563c03d1 -r 5b649fb2f2e1 NEWS
--- a/NEWS	Wed Nov 26 15:44:32 2014 +0100
+++ b/NEWS	Wed Nov 26 16:55:43 2014 +0100
@@ -220,8 +220,9 @@
 * Tactical PARALLEL_ALLGOALS is the most common way to refer to
 PARALLEL_GOALS.
 
-* Basic combinators map, fold, fold_map, split_list are available as
-parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
+* Basic combinators map, fold, fold_map, split_list, apply are
+available as parameterized antiquotations, e.g. @{map 4} for lists of
+quadruples.
 
 
 *** System ***
diff -r cbe9563c03d1 -r 5b649fb2f2e1 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Nov 26 15:44:32 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Nov 26 16:55:43 2014 +0100
@@ -6,10 +6,6 @@
 
 signature PREDICATE_COMPILE_AUX =
 sig
-  (* general functions *)
-  val apfst3 : ('a -> 'd) -> 'a * 'b * 'c -> 'd * 'b * 'c
-  val apsnd3 : ('b -> 'd) -> 'a * 'b * 'c -> 'a * 'd * 'c
-  val aptrd3 : ('c -> 'd) -> 'a * 'b * 'c -> 'a * 'b * 'd
   val find_indices : ('a -> bool) -> 'a list -> int list
   (* mode *)
   datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
@@ -172,10 +168,6 @@
 
 (* general functions *)
 
-fun apfst3 f (x, y, z) = (f x, y, z)
-fun apsnd3 f (x, y, z) = (x, f y, z)
-fun aptrd3 f (x, y, z) = (x, y, f z)
-
 fun comb_option f (SOME x1, SOME x2) = SOME (f (x1, x2))
   | comb_option f (NONE, SOME x2) = SOME x2
   | comb_option f (SOME x1, NONE) = SOME x1
diff -r cbe9563c03d1 -r 5b649fb2f2e1 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Nov 26 15:44:32 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Nov 26 16:55:43 2014 +0100
@@ -49,17 +49,18 @@
 fun mk_data (c, k, s) = {ignore_consts = c, keep_functions = k, processed_specs = s}
 fun map_data f {ignore_consts = c, keep_functions = k, processed_specs = s} = mk_data (f (c, k, s))
 
-fun ignore_consts cs = Data.map (map_data (apfst3 (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
+fun ignore_consts cs =
+  Data.map (map_data (@{apply 3(1)} (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
 
-fun keep_functions cs = Data.map (map_data (apsnd3 (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
+fun keep_functions cs =
+  Data.map (map_data (@{apply 3(2)} (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
 
 fun keep_function thy = Symtab.defined (#keep_functions (Data.get thy))
 
 fun processed_specs thy = Symtab.lookup (#processed_specs (Data.get thy))
 
 fun store_processed_specs (constname, specs) =
-  Data.map (map_data (aptrd3 (Symtab.update_new (constname, specs))))
-(* *)
+  Data.map (map_data (@{apply 3(3)} (Symtab.update_new (constname, specs))))
 
 
 fun defining_term_of_introrule_term t =
diff -r cbe9563c03d1 -r 5b649fb2f2e1 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Wed Nov 26 15:44:32 2014 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML	Wed Nov 26 16:55:43 2014 +0100
@@ -226,7 +226,21 @@
       \      | split_list" ^ tuple_cons n ^ " =\n\
       \          let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\
       \          in " ^ cons_tuple n ^ "end\n\
-      \  in split_list list end")))
+      \  in split_list list end")) #>
+  ML_Antiquotation.value @{binding apply}
+    (Scan.lift (parameter -- Scan.option (Args.parens (Parse.position Parse.nat))) >>
+      (fn (n, opt_index) =>
+        let
+          val cond =
+            (case opt_index of
+              NONE => K true
+            | SOME (index, index_pos) =>
+                if 1 <= index andalso index <= n then equal (string_of_int index)
+                else error ("Bad index: " ^ string_of_int index ^ Position.here index_pos));
+        in
+          "fn f => fn " ^ tuple_vars "x" n ^ " => " ^
+            tuple (map (fn a => (if cond a then "f x" else "x") ^ a) (indices n))
+        end)));
 
 end;
 
diff -r cbe9563c03d1 -r 5b649fb2f2e1 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed Nov 26 15:44:32 2014 +0100
+++ b/src/Tools/induct.ML	Wed Nov 26 16:55:43 2014 +0100
@@ -300,17 +300,12 @@
   Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs =>
     fold Item_Net.remove (filter_rules rs th) rs))));
 
-fun map1 f (x, y, z, s) = (f x, y, z, s);
-fun map2 f (x, y, z, s) = (x, f y, z, s);
-fun map3 f (x, y, z, s) = (x, y, f z, s);
-fun map4 f (x, y, z, s) = (x, y, z, f s);
-
-fun add_casesT rule x = map1 (apfst (Item_Net.update rule)) x;
-fun add_casesP rule x = map1 (apsnd (Item_Net.update rule)) x;
-fun add_inductT rule x = map2 (apfst (Item_Net.update rule)) x;
-fun add_inductP rule x = map2 (apsnd (Item_Net.update rule)) x;
-fun add_coinductT rule x = map3 (apfst (Item_Net.update rule)) x;
-fun add_coinductP rule x = map3 (apsnd (Item_Net.update rule)) x;
+fun add_casesT rule x = @{apply 4(1)} (apfst (Item_Net.update rule)) x;
+fun add_casesP rule x = @{apply 4(1)} (apsnd (Item_Net.update rule)) x;
+fun add_inductT rule x = @{apply 4(2)} (apfst (Item_Net.update rule)) x;
+fun add_inductP rule x = @{apply 4(2)} (apsnd (Item_Net.update rule)) x;
+fun add_coinductT rule x = @{apply 4(3)} (apfst (Item_Net.update rule)) x;
+fun add_coinductP rule x = @{apply 4(3)} (apsnd (Item_Net.update rule)) x;
 
 val consumes0 = Rule_Cases.default_consumes 0;
 val consumes1 = Rule_Cases.default_consumes 1;
@@ -319,18 +314,18 @@
 
 val cases_type = mk_att add_casesT consumes0;
 val cases_pred = mk_att add_casesP consumes1;
-val cases_del = del_att map1;
+val cases_del = del_att @{apply 4(1)};
 
 val induct_type = mk_att add_inductT consumes0;
 val induct_pred = mk_att add_inductP consumes1;
-val induct_del = del_att map2;
+val induct_del = del_att @{apply 4(2)};
 
 val coinduct_type = mk_att add_coinductT consumes0;
 val coinduct_pred = mk_att add_coinductP consumes1;
-val coinduct_del = del_att map3;
+val coinduct_del = del_att @{apply 4(3)};
 
 fun map_simpset f context =
-  context |> (Data.map o map4 o Simplifier.simpset_map (Context.proof_of context)) f;
+  context |> (Data.map o @{apply 4(4)} o Simplifier.simpset_map (Context.proof_of context)) f;
 
 fun induct_simp f =
   Thm.declaration_attribute (fn thm => map_simpset (fn ctxt => f (ctxt, [thm])));