--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Feb 14 15:03:23 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Feb 14 15:03:24 2014 +0100
@@ -162,8 +162,8 @@
val perm_fun_arg_Tssss =
mk_iter_fun_arg_types perm_ctr_Tsss perm_ns perm_mss (co_rec_of ctor_iters1);
- fun unpermute0 perm0_xs = permute_like (op =) perm0_kks kks perm0_xs;
- fun unpermute perm_xs = permute_like (op =) perm_indices indices perm_xs;
+ fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs;
+ fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs;
val induct_thms = unpermute0 (conj_dests nn induct_thm);