1.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Jun 01 11:58:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Jun 01 12:20:08 2010 +0200
     1.3 @@ -910,14 +910,14 @@
     1.4                                  \add_axioms_for_term",
     1.5                                  "too many nested axioms (" ^
     1.6                                  string_of_int depth ^ ")")
     1.7 -             else if Refute.is_const_of_class thy x then
     1.8 +             else if is_of_class_const thy x then
     1.9                 let
    1.10                   val class = Logic.class_of_const s
    1.11                   val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
    1.12                                                     class)
    1.13                   val ax1 = try (specialize_type thy x) of_class
    1.14                   val ax2 = Option.map (specialize_type thy x o snd)
    1.15 -                                      (Refute.get_classdef thy class)
    1.16 +                                      (get_class_def thy class)
    1.17                 in
    1.18                   fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
    1.19                        accum