# HG changeset patch
# User blanchet
# Date 1367500139 -7200
# Node ID 0a04c2a89ea9e26abf6f08196c7384fd9a5bdc7f
# Parent  75655198442e036b25fb90df9418a5c94beaf9d6
one more lib function

diff -r 75655198442e -r 0a04c2a89ea9 src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu May 02 14:04:56 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu May 02 15:08:59 2013 +0200
@@ -102,7 +102,7 @@
 val safe_elim_attrs = @{attributes [elim!]};
 val simp_attrs = @{attributes [simp]};
 
-fun unflat_lookup eq ys zs = map (map (fn x => nth zs (find_index (curry eq x) ys)));
+fun unflat_lookup eq = map oo unsort eq;
 
 fun mk_half_pairss' _ ([], []) = []
   | mk_half_pairss' indent (x :: xs, _ :: ys) =
diff -r 75655198442e -r 0a04c2a89ea9 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Thu May 02 14:04:56 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Thu May 02 15:08:59 2013 +0200
@@ -48,6 +48,7 @@
     'i list -> 'j -> 'k list * 'j
   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 seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
   val pad_list: 'a -> int -> 'a list -> 'a list
 
@@ -646,6 +647,8 @@
   | 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 seq_conds f n k xs =
   if k = n then
     map (f false) (take (k - 1) xs)