diff -r 63466160ff27 -r 5e960a0780a2 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat Jul 04 23:25:28 2009 +0200
+++ b/src/Pure/Isar/class.ML	Mon Jul 06 19:58:52 2009 +0200
@@ -83,7 +83,7 @@
       (fst (Locale.intros_of thy class));
 
     (* of_class *)
-    val of_class_prop_concl = Logic.mk_inclass (aT, class);
+    val of_class_prop_concl = Logic.mk_of_class (aT, class);
     val of_class_prop = case prop of NONE => of_class_prop_concl
       | SOME prop => Logic.mk_implies (Morphism.term const_morph
           ((map_types o map_atyps) (K aT) prop), of_class_prop_concl);