# HG changeset patch
# User blanchet
# Date 1444125023 -7200
# Node ID 24b5e7579fdd87c8c8704c077e300bbc15c4b160
# Parent  22378817612ff0154044647de584702e29f8f116
compile

diff -r 22378817612f -r 24b5e7579fdd src/HOL/Library/Multiset.thy
--- 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) =>
diff -r 22378817612f -r 24b5e7579fdd src/HOL/Tools/Nitpick/nitpick_model.ML
--- 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 :