src/HOL/Tools/Nitpick/nitpick_kodkod.ML
changeset 46085 447cda88adfe
parent 46083 efeaa79f021b
child 46086 096697aec8a7
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Jan 03 18:33:17 2012 +0100
@@ -1423,8 +1423,9 @@
         | Atom (k, _) =>
           let
             val dom_card = card_of_rep (rep_of arg_u)
-            val ran_R = Atom (exact_root dom_card k,
-                              offset_of_type ofs (range_type (type_of func_u)))
+            val ran_R =
+              Atom (exact_root dom_card k,
+                    offset_of_type ofs (pseudo_range_type (type_of func_u)))
           in
             to_apply_vect dom_card ran_R res_R (to_vect dom_card ran_R func_u)
                           arg_u