# HG changeset patch
# User blanchet
# Date 1325675393 -3600
# Node ID 31bc296a1257c9c9fefa0ef443c6fc5db9aaa4d9
# Parent  cd49d458b5452fc65f1432b51b7807b893abc805
handle higher-order occurrences of sets gracefully in model display

diff -r cd49d458b545 -r 31bc296a1257 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Jan 04 11:01:08 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Jan 04 12:09:53 2012 +0100
@@ -473,18 +473,25 @@
             #> format_fun (uniterize_unarize_unbox_etc_type T')
                           (uniterize_unarize_unbox_etc_type T1)
                           (uniterize_unarize_unbox_etc_type T2))
-    fun term_for_atom seen (T as Type (@{type_name fun}, [T1, T2])) T' j _ =
+
+
+    fun term_for_fun_or_set seen T T' j =
         let
-          val k1 = card_of_type card_assigns T1
-          val k2 = card_of_type card_assigns T2
+          val k1 = card_of_type card_assigns (pseudo_domain_type T)
+          val k2 = card_of_type card_assigns (pseudo_range_type T)
         in
           term_for_rep true seen T T' (Vect (k1, Atom (k2, 0)))
                        [nth_combination (replicate k1 (k2, 0)) j]
           handle General.Subscript =>
-                 raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom",
+                 raise ARG ("Nitpick_Model.reconstruct_term.\
+                            \term_for_fun_or_set",
                             signed_string_of_int j ^ " for " ^
                             string_for_rep (Vect (k1, Atom (k2, 0))))
         end
+    and term_for_atom seen (T as Type (@{type_name fun}, _)) T' j _ =
+        term_for_fun_or_set seen T T' j
+      | term_for_atom seen (T as Type (@{type_name set}, _)) T' j _ =
+        term_for_fun_or_set seen T T' j
       | term_for_atom seen (Type (@{type_name prod}, [T1, T2])) _ j k =
         let
           val k1 = card_of_type card_assigns T1
@@ -492,7 +499,8 @@
         in
           list_comb (HOLogic.pair_const T1 T2,
                      map3 (fn T => term_for_atom seen T T) [T1, T2]
-                          [j div k2, j mod k2] [k1, k2]) (* ### k2 or k1? FIXME *)
+                          (* ### k2 or k1? FIXME *)
+                          [j div k2, j mod k2] [k1, k2])
         end
       | term_for_atom seen @{typ prop} _ j k =
         HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k)