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.
compile
authorblanchet
Tue, 06 Oct 2015 11:50:23 +0200
changeset 61333 24b5e7579fdd
parent 61332 22378817612f
child 61334 8d40ddaa427f
compile
src/HOL/Library/Multiset.thy file | annotate | diff | comparison | revisions
src/HOL/Tools/Nitpick/nitpick_model.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Multiset.thy	Tue Oct 06 11:34:07 2015 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Oct 06 11:50:23 2015 +0200
@@ -2048,7 +2048,7 @@
               | NONE => [Const (maybe_name, elem_T --> elem_T) $ t])
           in
             (case maps elems_for (all_values elem_T) @
-                 (if maybe_opt then [Const (Nitpick_Model.unrep (), elem_T)] else []) of
+                 (if maybe_opt then [Const (Nitpick_Model.unrep_mixfix (), elem_T)] else []) of
               [] => Const (@{const_name zero_class.zero}, T)
             | ts =>
                 foldl1 (fn (t1, t2) =>
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Oct 06 11:34:07 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Oct 06 11:50:23 2015 +0200
@@ -23,6 +23,7 @@
 
   val irrelevant : string
   val unknown : string
+  val unrep_mixfix : unit -> string
   val register_term_postprocessor :
     typ -> term_postprocessor -> morphism -> Context.generic -> Context.generic
   val register_term_postprocessor_global :
isabelle