--- a/src/HOL/BNF/Tools/bnf_comp.ML Fri Aug 16 18:56:33 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Fri Aug 16 19:03:31 2013 +0200
@@ -445,8 +445,8 @@
val live = live_of_bnf bnf;
val dead = dead_of_bnf bnf;
val nwits = nwits_of_bnf bnf;
- fun permute xs = mk_permute (op =) src dest xs;
- fun unpermute xs = mk_permute (op =) dest src xs;
+ fun permute xs = permute_like (op =) src dest xs;
+ fun unpermute xs = permute_like (op =) dest src xs;
val (Ds, lthy1) = apfst (map TFree)
(Variable.invent_types (replicate dead HOLogic.typeS) lthy);