# HG changeset patch
# User traytel
# Date 1376314615 -7200
# Node ID 9e22d62642776ae41c80c1cc189c7186788644b0
# Parent  2ab38527aca75b22499a5250d2d6f279f3e8b0b8
generalized library function

diff -r 2ab38527aca7 -r 9e22d6264277 src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Mon Aug 12 18:03:47 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Mon Aug 12 15:36:55 2013 +0200
@@ -524,8 +524,8 @@
 fun normalize_bnfs qualify Ass Ds sort bnfs unfold_set lthy =
   let
     val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass;
-    val kill_poss = map (find_indices Ds) Ass;
-    val live_poss = map2 (subtract (op =)) kill_poss before_kill_src;
+    val kill_poss = map (find_indices op = Ds) Ass;
+    val live_poss = map2 (subtract op =) kill_poss before_kill_src;
     val before_kill_dest = map2 append kill_poss live_poss;
     val kill_ns = map length kill_poss;
     val (inners', (unfold_set', lthy')) =
@@ -537,7 +537,7 @@
     val As = sort Ass';
     val after_lift_dest = replicate (length Ass') (0 upto (length As - 1));
     val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass';
-    val new_poss = map2 (subtract (op =)) old_poss after_lift_dest;
+    val new_poss = map2 (subtract op =) old_poss after_lift_dest;
     val after_lift_src = map2 append new_poss old_poss;
     val lift_ns = map (fn xs => length As - length xs) Ass';
   in
@@ -673,7 +673,7 @@
               in qualify' o Binding.qualify true namei end;
             val odead = dead_of_bnf bnf;
             val olive = live_of_bnf bnf;
-            val oDs_pos = find_indices [TFree ("dead", [])] (snd (Term.dest_Type
+            val oDs_pos = find_indices op = [TFree ("dead", [])] (snd (Term.dest_Type
               (mk_T_of_bnf (replicate odead (TFree ("dead", []))) (replicate olive dummyT) bnf)));
             val oDs = map (nth Ts) oDs_pos;
             val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
diff -r 2ab38527aca7 -r 9e22d6264277 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Mon Aug 12 18:03:47 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Mon Aug 12 15:36:55 2013 +0200
@@ -163,7 +163,7 @@
   val unfold_thms: Proof.context -> thm list -> thm -> thm
 
   val mk_permute: ''a list -> ''a list -> 'b list -> 'b list
-  val find_indices: ''a list -> ''a list -> int list
+  val find_indices: ('b * 'a -> bool) -> 'a list -> 'b list -> int list
 
   val certifyT: Proof.context -> typ -> ctyp
   val certify: Proof.context -> term -> cterm
@@ -616,8 +616,8 @@
     let val (x, T) = Term.dest_Free free;
     in HOLogic.exists_const T $ Term.absfree (x, T) P end);
 
-fun find_indices xs ys = map_filter I
-  (map_index (fn (i, y) => if member (op =) xs y then SOME i else NONE) ys);
+fun find_indices eq xs ys = map_filter I
+  (map_index (fn (i, y) => if member eq xs y then SOME i else NONE) ys);
 
 fun mk_trans thm1 thm2 = trans OF [thm1, thm2];
 fun mk_sym thm = thm RS sym;
@@ -700,6 +700,7 @@
   | transpose ([] :: xss) = transpose xss
   | transpose xss = map hd xss :: transpose (map tl xss);
 
+(*FIXME: merge with mk_permute*)
 fun sort_like eq xs ys = map (fn x => nth ys (find_index (curry eq x) xs));
 
 fun seq_conds f n k xs =