src/HOL/Library/Multiset.thy
changeset 37261 8a89fd40ed0b
parent 37169 f69efa106feb
child 37751 89e16802b6cc
--- 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)