changeset 31943 | 5e960a0780a2 |
parent 31904 | a86896359ca4 |
child 31944 | c8a35979a5bc |
--- 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);