src/Pure/Isar/class_target.ML
changeset 32800 57fcca4e7c0e
parent 32074 76d6ba08a05f
child 32805 9b535493ac8d
     1.1 --- a/src/Pure/Isar/class_target.ML	Fri Aug 14 21:36:14 2009 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Wed Aug 19 19:35:46 2009 +0200
     1.3 @@ -210,7 +210,7 @@
     1.4  fun activate_defs class thms thy =
     1.5    let
     1.6      val eq_morph = Element.eq_morphism thy thms;
     1.7 -    fun amend cls thy = Locale.amend_registration eq_morph
     1.8 +    fun amend cls thy = Locale.amend_registration_legacy eq_morph
     1.9        (cls, morphism thy cls) thy;
    1.10    in fold amend (heritage thy [class]) thy end;
    1.11