# HG changeset patch
# User wenzelm
# Date 1536493488 -7200
# Node ID b85d509e7cbf9b60e63e6aa3b611ed4fca8082e1
# Parent  d4223afddd478c9ce07234ac4a4a4b4f4e3600be
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";

diff -r d4223afddd47 -r b85d509e7cbf src/HOL/Tools/BNF/bnf_comp.ML
--- 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;