Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned -- no position;
authorwenzelm
Fri, 15 Apr 2016 13:02:23 +0200
changeset 62990 7b0f0398d33f
parent 62989 ed8739792e8a
child 62991 35f1475e9ced
tuned -- no position;
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML file | annotate | diff | comparison | revisions 
--- 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 () =
isabelle