# HG changeset patch
# User blanchet
# Date 1376672611 -7200
# Node ID e6edd7abc4ceb698c3909ebfabfdf2e4666bebd2
# Parent  476db75906ae02a0f08bc2a5e603d9bdd2721f30
renamed function

diff -r 476db75906ae -r e6edd7abc4ce src/HOL/BNF/Tools/bnf_comp.ML
--- 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);
diff -r 476db75906ae -r e6edd7abc4ce src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- 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) =
diff -r 476db75906ae -r e6edd7abc4ce src/HOL/BNF/Tools/bnf_def.ML
--- 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*)
diff -r 476db75906ae -r e6edd7abc4ce src/HOL/BNF/Tools/bnf_util.ML
--- 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