# HG changeset patch
# User blanchet
# Date 1266933044 -3600
# Node ID 22442ab3e7a3504e658e9bd369aedef068f60209
# Parent  450ab945c4513250555a240513c73a70656525e0
optimized multisets in Nitpick by fishing "finite"

diff -r 450ab945c451 -r 22442ab3e7a3 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Feb 23 14:11:36 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Feb 23 14:50:44 2010 +0100
@@ -619,12 +619,19 @@
 fun is_univ_typedef thy (Type (s, _)) =
     (case typedef_info thy s of
        SOME {set_def, prop_of_Rep, ...} =>
-       (case set_def of
-          SOME thm =>
-          try (fst o dest_Const o snd o Logic.dest_equals o prop_of) thm
-        | NONE =>
-          try (fst o dest_Const o snd o HOLogic.dest_mem
-               o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top}
+       let
+         val t_opt =
+           case set_def of
+             SOME thm => try (snd o Logic.dest_equals o prop_of) thm
+           | NONE => try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop)
+                         prop_of_Rep
+       in
+         case t_opt of
+           SOME (Const (@{const_name top}, _)) => true
+         | SOME (Const (@{const_name Collect}, _)
+                 $ Abs (_, _, Const (@{const_name finite}, _) $ _)) => true
+         | _ => false
+       end
      | NONE => false)
   | is_univ_typedef _ _ = false
 (* theory -> (typ option * bool) list -> typ -> bool *)