src/Pure/Isar/class.ML
changeset 31943 5e960a0780a2
parent 31904 a86896359ca4
child 31944 c8a35979a5bc
     1.1 --- a/src/Pure/Isar/class.ML	Sat Jul 04 23:25:28 2009 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Jul 06 19:58:52 2009 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4        (fst (Locale.intros_of thy class));
     1.5  
     1.6      (* of_class *)
     1.7 -    val of_class_prop_concl = Logic.mk_inclass (aT, class);
     1.8 +    val of_class_prop_concl = Logic.mk_of_class (aT, class);
     1.9      val of_class_prop = case prop of NONE => of_class_prop_concl
    1.10        | SOME prop => Logic.mk_implies (Morphism.term const_morph
    1.11            ((map_types o map_atyps) (K aT) prop), of_class_prop_concl);