# HG changeset patch
# User blanchet
# Date 1369996119 -7200
# Node ID 1d37d281645d989f23370bfab6052f085c19c912
# Parent  39d60668f8dfa227ff126279b77e26bd26fcd19f
renamed util function

diff -r 39d60668f8df -r 1d37d281645d src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Fri May 31 12:00:18 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Fri May 31 12:28:39 2013 +0200
@@ -102,7 +102,7 @@
 val safe_elim_attrs = @{attributes [elim!]};
 val simp_attrs = @{attributes [simp]};
 
-fun unflat_lookup eq = map oo unsort eq;
+fun unflat_lookup eq = map oo sort_like eq;
 
 fun mk_half_pairss' _ ([], []) = []
   | mk_half_pairss' indent (x :: xs, _ :: ys) =
diff -r 39d60668f8df -r 1d37d281645d src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Fri May 31 12:00:18 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri May 31 12:28:39 2013 +0200
@@ -49,7 +49,7 @@
   val split_list4: ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list
   val splice: 'a list -> 'a list -> 'a list
   val transpose: 'a list list -> 'a list list
-  val unsort: ('a * 'b -> bool) -> 'b list -> 'c list -> 'a list -> 'c list
+  val sort_like: ('a * 'b -> bool) -> 'b list -> 'c list -> 'a list -> 'c list
   val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
   val pad_list: 'a -> int -> 'a list -> 'a list
 
@@ -676,7 +676,7 @@
   | transpose ([] :: xss) = transpose xss
   | transpose xss = map hd xss :: transpose (map tl xss);
 
-fun unsort eq ys zs = map (fn x => nth zs (find_index (curry eq x) ys));
+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