# HG changeset patch
# User wenzelm
# Date 1407927567 -7200
# Node ID 2bd92d3f92d7387721fb38f6c159aa3f2bd74b8f
# Parent  a3360da1d2f0c274130673052c94c954fda81aa1
clarified terminology: first is top (amending d110b0d1bc12);

diff -r a3360da1d2f0 -r 2bd92d3f92d7 src/Pure/Isar/local_theory.ML
--- 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));