src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 45980 af59825c40cf
parent 45797 977cf00fb8d3
child 46081 8f6465f7021b
--- 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