clarified terminology: first is top (amending d110b0d1bc12);

--- a/src/Pure/Isar/local_theory.ML	Wed Aug 13 12:52:26 2014 +0200
+++ b/src/Pure/Isar/local_theory.ML	Wed Aug 13 12:59:27 2014 +0200
@@ -115,7 +115,7 @@
 val bottom_of = List.last o Data.get o assert;
 val top_of = hd o Data.get o assert;
 
-fun map_bottom f =
+fun map_top f =
   assert #>
   Data.map (fn {naming, operations, after_close, brittle, target} :: parents =>
     make_lthy (f (naming, operations, after_close, brittle, target)) :: parents);
@@ -163,7 +163,7 @@
 
 fun mark_brittle lthy =
   if level lthy = 1 then
-    map_bottom (fn (naming, operations, after_close, brittle, target) =>
+    map_top (fn (naming, operations, after_close, brittle, target) =>
       (naming, operations, after_close, true, target)) lthy
   else lthy;
 
@@ -178,7 +178,7 @@
 val full_name = Name_Space.full_name o naming_of;
 
 fun map_naming f =
-  map_bottom (fn (naming, operations, after_close, brittle, target) =>
+  map_top (fn (naming, operations, after_close, brittle, target) =>
     (f naming, operations, after_close, brittle, target));
 
 val conceal = map_naming Name_Space.conceal;
@@ -310,7 +310,7 @@
 (* activation of locale fragments *)
 
 fun activate_nonbrittle dep_morph mixin export =
-  map_bottom (fn (naming, operations, after_close, brittle, target) =>
+  map_top (fn (naming, operations, after_close, brittle, target) =>
     (naming, operations, after_close, brittle,
       (Context.proof_map ooo Locale.add_registration) dep_morph mixin export target));