--- a/src/HOL/Tools/BNF/bnf_comp.ML Fri Feb 14 15:03:23 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Fri Feb 14 15:03:24 2014 +0100
@@ -449,8 +449,9 @@
val live = live_of_bnf bnf;
val dead = dead_of_bnf bnf;
val nwits = nwits_of_bnf bnf;
- fun permute xs = permute_like (op =) src dest xs;
- fun unpermute xs = permute_like (op =) dest src xs;
+
+ fun permute xs = permute_like_unique (op =) src dest xs;
+ fun unpermute xs = permute_like_unique (op =) dest src xs;
val (Ds, lthy1) = apfst (map TFree)
(Variable.invent_types (replicate dead HOLogic.typeS) lthy);