# HG changeset patch
# User ballarin
# Date 1250703346 -7200
# Node ID 57fcca4e7c0eff946562813c352306928f8a4923
# Parent  99dc5b7b468704e5312f54510babb01a6b7c5abd
Improved comments and api names.

diff -r 99dc5b7b4687 -r 57fcca4e7c0e src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Fri Aug 14 21:36:14 2009 +0200
+++ b/src/Pure/Isar/class_target.ML	Wed Aug 19 19:35:46 2009 +0200
@@ -210,7 +210,7 @@
 fun activate_defs class thms thy =
   let
     val eq_morph = Element.eq_morphism thy thms;
-    fun amend cls thy = Locale.amend_registration eq_morph
+    fun amend cls thy = Locale.amend_registration_legacy eq_morph
       (cls, morphism thy cls) thy;
   in fold amend (heritage thy [class]) thy end;
 
diff -r 99dc5b7b4687 -r 57fcca4e7c0e src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Aug 14 21:36:14 2009 +0200
+++ b/src/Pure/Isar/expression.ML	Wed Aug 19 19:35:46 2009 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Isar/expression.ML
     Author:     Clemens Ballarin, TU Muenchen
 
-Locale expressions.
+Locale expressions and user interface layer of locales.
 *)
 
 signature EXPRESSION =
diff -r 99dc5b7b4687 -r 57fcca4e7c0e src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Aug 14 21:36:14 2009 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Aug 19 19:35:46 2009 +0200
@@ -69,7 +69,7 @@
 
   (* Registrations and dependencies *)
   val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
-  val amend_registration: morphism -> string * morphism -> theory -> theory
+  val amend_registration_legacy: morphism -> string * morphism -> theory -> theory
   val add_dependency: string -> string * morphism -> morphism -> theory -> theory
 
   (* Diagnostic *)
@@ -239,7 +239,7 @@
     (* Find all dependencies incuding new ones (which are dependencies enriching
       existing registrations). *)
     val (dependencies, marked') = add thy 0 (name, morph) ([], []);
-    (* Filter out exisiting fragments. *)
+    (* Filter out fragments from marked; these won't be activated. *)
     val dependencies' = filter_out (fn (name, morph) =>
       member (ident_eq thy) marked (name, instance_of thy name morph)) dependencies;
   in
@@ -344,7 +344,8 @@
 fun all_registrations thy = Registrations.get thy
   |> map reg_morph;
 
-fun amend_registration morph (name, base_morph) thy =
+fun amend_registration_legacy morph (name, base_morph) thy =
+  (* legacy, never modify base morphism *)
   let
     val regs = map #1 (Registrations.get thy);
     val base = instance_of thy name base_morph;