smash position to avoid position of other file "~~/src/HOL/BNF_Composition.thy" (due to "bnf ID"), e.g. relevant for "HOL-Nominal-Examples.Class1";
--- a/src/HOL/Tools/BNF/bnf_comp.ML Sun Sep 09 13:40:14 2018 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Sun Sep 09 13:44:48 2018 +0200
@@ -615,7 +615,7 @@
fun raw_permute_bnf qualify src dest bnf (accum as (unfold_set, lthy)) =
if src = dest then (bnf, accum) else
let
- val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf);
+ val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf) |> Binding.reset_pos;
val live = live_of_bnf bnf;
val deads = deads_of_bnf bnf;
val nwits = nwits_of_bnf bnf;