src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 45980 af59825c40cf
parent 45797 977cf00fb8d3
child 46081 8f6465f7021b
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Dec 24 16:14:58 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Dec 24 16:14:58 2011 +0100
     1.3 @@ -545,7 +545,7 @@
     1.4    if is_frac_type ctxt (Type (s, [])) then
     1.5      SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
     1.6            Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
     1.7 -          set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
     1.8 +          set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Collect Frac"}
     1.9                            |> Logic.varify_global,
    1.10            set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
    1.11    else case Typedef.get_info ctxt s of