src/HOL/Tools/BNF/bnf_comp.ML
changeset 68960 b85d509e7cbf
parent 67091 1393c2340eec
child 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Sun Sep 09 13:40:14 2018 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sun Sep 09 13:44:48 2018 +0200
     1.3 @@ -615,7 +615,7 @@
     1.4  fun raw_permute_bnf qualify src dest bnf (accum as (unfold_set, lthy)) =
     1.5    if src = dest then (bnf, accum) else
     1.6    let
     1.7 -    val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf);
     1.8 +    val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf) |> Binding.reset_pos;
     1.9      val live = live_of_bnf bnf;
    1.10      val deads = deads_of_bnf bnf;
    1.11      val nwits = nwits_of_bnf bnf;