1.1 --- a/src/Pure/axclass.ML	Sat Jul 04 23:25:28 2009 +0200
     1.2 +++ b/src/Pure/axclass.ML	Mon Jul 06 19:58:52 2009 +0200
     1.3 @@ -470,9 +470,9 @@
     1.4  
     1.5      (* definition *)
     1.6  
     1.7 -    val conjs = map (curry Logic.mk_inclass (Term.aT [])) super @ flat axiomss;
     1.8 +    val conjs = map (curry Logic.mk_of_class (Term.aT [])) super @ flat axiomss;
     1.9      val class_eq =
    1.10 -      Logic.mk_equals (Logic.mk_inclass (Term.aT [], class), Logic.mk_conjunction_balanced conjs);
    1.11 +      Logic.mk_equals (Logic.mk_of_class (Term.aT [], class), Logic.mk_conjunction_balanced conjs);
    1.12  
    1.13      val ([def], def_thy) =
    1.14        thy
    1.15 @@ -605,7 +605,7 @@
    1.16      val ths =
    1.17        sort |> map (fn c =>
    1.18          Goal.finish (the (lookup_type cache' typ c) RS
    1.19 -          Goal.init (Thm.cterm_of thy (Logic.mk_inclass (typ, c))))
    1.20 +          Goal.init (Thm.cterm_of thy (Logic.mk_of_class (typ, c))))
    1.21          |> Thm.adjust_maxidx_thm ~1);
    1.22    in (ths, cache') end;
    1.23