adjusted to set/pred distinction by means of type constructor `set`
authorhaftmann
Sat, 24 Dec 2011 16:14:58 +0100
changeset 45980 af59825c40cf
parent 45979 296d9a9c8d24
child 45981 4c629115e3ab
adjusted to set/pred distinction by means of type constructor `set`
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