src/Pure/Isar/class_target.ML
changeset 38107 3a46cebd7983
parent 37678 0040bafffdef
child 38348 cf7b2121ad9d
--- a/src/Pure/Isar/class_target.ML	Fri Jul 30 15:03:42 2010 +0200
+++ b/src/Pure/Isar/class_target.ML	Sat Jul 31 21:14:20 2010 +0200
@@ -205,8 +205,8 @@
 
 fun activate_defs class thms thy = case Element.eq_morphism thy thms
  of SOME eq_morph => fold (fn cls => fn thy =>
-      Locale.amend_registration (cls, base_morphism thy cls)
-        (eq_morph, true) (export_morphism thy cls) thy) (heritage thy [class]) thy
+      Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls)
+        (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy
   | NONE => thy;
 
 fun register_operation class (c, (t, some_def)) thy =