# HG changeset patch
# User wenzelm
# Date 1460718143 -7200
# Node ID 7b0f0398d33f3306f233442bf528fc204b0c4f4f
# Parent  ed8739792e8a17a46586ff5671732fb2eb93b82b
tuned -- no position;

diff -r ed8739792e8a -r 7b0f0398d33f src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Apr 15 13:01:45 2016 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Apr 15 13:02:23 2016 +0200
@@ -1960,7 +1960,7 @@
     val setT = HOLogic.mk_setT T
     val elems = HOLogic.mk_set T ts
     val ([dots], ctxt') = ctxt
-      |> Proof_Context.add_fixes [(@{binding dots}, SOME setT, Mixfix.mixfix "...")]
+      |> Proof_Context.add_fixes [(Binding.name "dots", SOME setT, Mixfix.mixfix "...")]
     (* check expected values *)
     val union = Const (@{const_abbrev Set.union}, setT --> setT --> setT)
     val () =