src/Pure/Isar/class_target.ML
changeset 36462 70a1e6accac3
parent 36328 4d9deabf6474
child 36610 bafd82950e24
     1.1 --- a/src/Pure/Isar/class_target.ML	Wed Apr 28 08:25:02 2010 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Wed Apr 28 13:30:17 2010 +0200
     1.3 @@ -209,6 +209,9 @@
     1.4        (eq_morph, true) (export_morphism thy cls) thy;
     1.5    in fold amend (heritage thy [class]) thy end;
     1.6  
     1.7 +(*fun activate_defs class thms thy = Locale.amend_registration (class, base_morphism thy class)
     1.8 +  (Element.eq_morphism thy thms, true) (export_morphism thy class) thy;*)
     1.9 +
    1.10  fun register_operation class (c, (t, some_def)) thy =
    1.11    let
    1.12      val base_sort = base_sort thy class;