# HG changeset patch
# User haftmann
# Date 1324739698 -3600
# Node ID af59825c40cf7f5893feaa9f82378bf8e61823d3
# Parent  296d9a9c8d24d63b24175573890229ba7cbc9e8e
adjusted to set/pred distinction by means of type constructor `set`

diff -r 296d9a9c8d24 -r af59825c40cf src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Dec 24 16:14:58 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Dec 24 16:14:58 2011 +0100
@@ -545,7 +545,7 @@
   if is_frac_type ctxt (Type (s, [])) then
     SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
           Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
-          set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
+          set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Collect Frac"}
                           |> Logic.varify_global,
           set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
   else case Typedef.get_info ctxt s of