compile
authorblanchet
Tue Oct 06 11:50:23 2015 +0200 (2015-10-06)
changeset 6133324b5e7579fdd
parent 61332 22378817612f
child 61334 8d40ddaa427f
compile
src/HOL/Library/Multiset.thy
src/HOL/Tools/Nitpick/nitpick_model.ML
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue Oct 06 11:34:07 2015 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue Oct 06 11:50:23 2015 +0200
     1.3 @@ -2048,7 +2048,7 @@
     1.4                | NONE => [Const (maybe_name, elem_T --> elem_T) $ t])
     1.5            in
     1.6              (case maps elems_for (all_values elem_T) @
     1.7 -                 (if maybe_opt then [Const (Nitpick_Model.unrep (), elem_T)] else []) of
     1.8 +                 (if maybe_opt then [Const (Nitpick_Model.unrep_mixfix (), elem_T)] else []) of
     1.9                [] => Const (@{const_name zero_class.zero}, T)
    1.10              | ts =>
    1.11                  foldl1 (fn (t1, t2) =>
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Oct 06 11:34:07 2015 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Oct 06 11:50:23 2015 +0200
     2.3 @@ -23,6 +23,7 @@
     2.4  
     2.5    val irrelevant : string
     2.6    val unknown : string
     2.7 +  val unrep_mixfix : unit -> string
     2.8    val register_term_postprocessor :
     2.9      typ -> term_postprocessor -> morphism -> Context.generic -> Context.generic
    2.10    val register_term_postprocessor_global :