# HG changeset patch
# User blanchet
# Date 1376672193 -7200
# Node ID 476db75906ae02a0f08bc2a5e603d9bdd2721f30
# Parent  dd5ea8a51af08c51fdd248899b19f9e20d0b5375
eliminate quasi-duplicate function

diff -r dd5ea8a51af0 -r 476db75906ae src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Fri Aug 16 18:45:57 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Fri Aug 16 18:56:33 2013 +0200
@@ -120,7 +120,7 @@
 val safe_elim_attrs = @{attributes [elim!]};
 val simp_attrs = @{attributes [simp]};
 
-fun unflat_lookup eq = map oo sort_like eq;
+fun unflat_lookup eq xs ys = map (fn xs' => mk_permute eq xs xs' ys);
 
 fun mk_half_pairss' _ ([], []) = []
   | mk_half_pairss' indent (x :: xs, _ :: ys) =
diff -r dd5ea8a51af0 -r 476db75906ae src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Fri Aug 16 18:45:57 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Fri Aug 16 18:56:33 2013 +0200
@@ -329,7 +329,7 @@
     val lives = lives_of_bnf bnf;
     val deads = deads_of_bnf bnf;
   in
-    sort_like (op =) (deads @ lives) (replicate (length deads) dead_x @ xs) Ts
+    mk_permute (op =) (deads @ lives) Ts (replicate (length deads) dead_x @ xs)
   end;
 
 (*terms*)
diff -r dd5ea8a51af0 -r 476db75906ae src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 16 18:45:57 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 16 18:56:33 2013 +0200
@@ -54,7 +54,6 @@
 
   val find_indices: ('b * 'a -> bool) -> 'a list -> 'b list -> int list
   val mk_permute: ('a * 'b -> bool) -> 'a list -> 'b list -> 'c list -> 'c list
-  val sort_like: ('a * 'b -> bool) -> 'b list -> 'c list -> 'a list -> 'c list
 
   val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context
   val mk_TFrees: int -> Proof.context -> typ list * Proof.context
@@ -722,9 +721,6 @@
 
 fun mk_permute eq xs xs' ys = map (nth ys o (fn y => find_index (fn x => eq (x, y)) xs)) xs';
 
-(*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 =
   if k = n then
     map (f false) (take (k - 1) xs)