# HG changeset patch
# User haftmann
# Date 1272454217 -7200
# Node ID 70a1e6accac369f515dce7de20dae2dd0e1b44fb
# Parent  06081e4921d618fe374022c4ed0988d35408b22c
codified comment

diff -r 06081e4921d6 -r 70a1e6accac3 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Wed Apr 28 08:25:02 2010 +0200
+++ b/src/Pure/Isar/class_target.ML	Wed Apr 28 13:30:17 2010 +0200
@@ -209,6 +209,9 @@
       (eq_morph, true) (export_morphism thy cls) thy;
   in fold amend (heritage thy [class]) thy end;
 
+(*fun activate_defs class thms thy = Locale.amend_registration (class, base_morphism thy class)
+  (Element.eq_morphism thy thms, true) (export_morphism thy class) thy;*)
+
 fun register_operation class (c, (t, some_def)) thy =
   let
     val base_sort = base_sort thy class;