Nitpick: show "..." in datatype values (e.g., [{0::nat, ...}]), since these are really equivalence classes
authorblanchet
Thu, 27 May 2010 17:22:16 +0200
changeset 37170 38ba15040455
parent 37169 f69efa106feb
child 37171 fc1e20373e6a
Nitpick: show "..." in datatype values (e.g., [{0::nat, ...}]), since these are really equivalence classes
src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu May 27 16:42:03 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu May 27 17:22:16 2010 +0200
@@ -587,7 +587,7 @@
       | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T'
                      (Vect (k, R')) [js] =
         term_for_vect seen k R' T1 T2 T' js
-      | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T'
+      | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
                      (Func (R1, Formula Neut)) jss =
         let
           val jss1 = all_combinations_for_rep R1
@@ -596,7 +596,7 @@
             map (fn js => term_for_rep true seen T2 T2 (Atom (2, 0))
                                        [[int_from_bool (member (op =) jss js)]])
                 jss1
-        in make_fun false T1 T2 T' ts1 ts2 end
+        in make_fun maybe_opt T1 T2 T' ts1 ts2 end
       | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
                      (Func (R1, R2)) jss =
         let