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";
authorwenzelm
Sun, 09 Sep 2018 13:44:48 +0200
changeset 68960 b85d509e7cbf
parent 68959 d4223afddd47
child 68961 22a3790eecae
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";
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;