src/HOL/Tools/BNF/bnf_comp.ML
changeset 55480 59cc4a8bc28a
parent 55197 5a54ed681ba2
child 55703 a21069381ba5
     1.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Fri Feb 14 15:03:23 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Fri Feb 14 15:03:24 2014 +0100
     1.3 @@ -449,8 +449,9 @@
     1.4      val live = live_of_bnf bnf;
     1.5      val dead = dead_of_bnf bnf;
     1.6      val nwits = nwits_of_bnf bnf;
     1.7 -    fun permute xs = permute_like (op =) src dest xs;
     1.8 -    fun unpermute xs = permute_like (op =) dest src xs;
     1.9 +
    1.10 +    fun permute xs = permute_like_unique (op =) src dest xs;
    1.11 +    fun unpermute xs = permute_like_unique (op =) dest src xs;
    1.12  
    1.13      val (Ds, lthy1) = apfst (map TFree)
    1.14        (Variable.invent_types (replicate dead HOLogic.typeS) lthy);