--- 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) =
--- 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*)
--- 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)