src/HOL/BNF/Tools/bnf_ctr_sugar.ML

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