--- a/src/HOL/BNF/Tools/bnf_comp.ML Fri Aug 16 18:56:33 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Fri Aug 16 19:03:31 2013 +0200
@@ -445,8 +445,8 @@
val live = live_of_bnf bnf;
val dead = dead_of_bnf bnf;
val nwits = nwits_of_bnf bnf;
- fun permute xs = mk_permute (op =) src dest xs;
- fun unpermute xs = mk_permute (op =) dest src xs;
+ fun permute xs = permute_like (op =) src dest xs;
+ fun unpermute xs = permute_like (op =) dest src xs;
val (Ds, lthy1) = apfst (map TFree)
(Variable.invent_types (replicate dead HOLogic.typeS) lthy);
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Fri Aug 16 18:56:33 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Fri Aug 16 19:03:31 2013 +0200
@@ -120,7 +120,7 @@
val safe_elim_attrs = @{attributes [elim!]};
val simp_attrs = @{attributes [simp]};
-fun unflat_lookup eq xs ys = map (fn xs' => mk_permute eq xs xs' ys);
+fun unflat_lookup eq xs ys = map (fn xs' => permute_like 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:56:33 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Fri Aug 16 19:03:31 2013 +0200
@@ -329,7 +329,7 @@
val lives = lives_of_bnf bnf;
val deads = deads_of_bnf bnf;
in
- mk_permute (op =) (deads @ lives) Ts (replicate (length deads) dead_x @ xs)
+ permute_like (op =) (deads @ lives) Ts (replicate (length deads) dead_x @ xs)
end;
(*terms*)
--- a/src/HOL/BNF/Tools/bnf_util.ML Fri Aug 16 18:56:33 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML Fri Aug 16 19:03:31 2013 +0200
@@ -53,7 +53,7 @@
val pad_list: 'a -> int -> 'a list -> 'a list
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 permute_like: ('a * 'b -> bool) -> 'a list -> 'b list -> 'c 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
@@ -719,7 +719,7 @@
| transpose ([] :: xss) = transpose xss
| transpose xss = map hd xss :: transpose (map tl xss);
-fun mk_permute eq xs xs' ys = map (nth ys o (fn y => find_index (fn x => eq (x, y)) xs)) xs';
+fun permute_like eq xs xs' ys = map (nth ys o (fn y => find_index (fn x => eq (x, y)) xs)) xs';
fun seq_conds f n k xs =
if k = n then