diff -r dde817e6dfb1 -r 8a89fd40ed0b src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Tue Jun 01 12:20:08 2010 +0200 +++ b/src/HOL/Library/Multiset.thy Tue Jun 01 14:14:02 2010 +0200 @@ -1711,7 +1711,8 @@ | 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 (), elem_T)] + else []) of [] => Const (@{const_name zero_class.zero}, T) | ts => foldl1 (fn (t1, t2) => Const (@{const_name plus_class.plus}, T --> T --> T)