# HG changeset patch
# User haftmann
# Date 1402263052 -7200
# Node ID d110b0d1bc12ed762d3b2b753a459f84c4123aad
# Parent  d59c4383cae45ccdcf094ffc3e028ddd665a8783
tuned terminology: emphasize stack-like nature of nested local theories

diff -r d59c4383cae4 -r d110b0d1bc12 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sun Jun 08 23:30:51 2014 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sun Jun 08 23:30:52 2014 +0200
@@ -112,15 +112,15 @@
 fun assert lthy =
   if null (Data.get lthy) then error "Missing local theory context" else lthy;
 
-val get_last_lthy = List.last o Data.get o assert;
-val get_first_lthy = hd o Data.get o assert;
+val bottom_of = List.last o Data.get o assert;
+val top_of = hd o Data.get o assert;
 
-fun map_first_lthy f =
+fun map_bottom f =
   assert #>
   Data.map (fn {naming, operations, after_close, brittle, target} :: parents =>
     make_lthy (f (naming, operations, after_close, brittle, target)) :: parents);
 
-fun restore lthy = #target (get_first_lthy lthy) |> Data.put (Data.get lthy);
+fun restore lthy = #target (top_of lthy) |> Data.put (Data.get lthy);
 
 
 (* nested structure *)
@@ -163,23 +163,23 @@
 
 fun mark_brittle lthy =
   if level lthy = 1
-  then map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
+  then map_bottom (fn (naming, operations, after_close, brittle, target) =>
     (naming, operations, after_close, true, target)) lthy
   else lthy;
 
 fun assert_nonbrittle lthy =
-  if #brittle (get_first_lthy lthy)
+  if #brittle (top_of lthy)
   then error "Brittle local theory context"
   else lthy;
 
 
 (* naming *)
 
-val naming_of = #naming o get_first_lthy;
+val naming_of = #naming o top_of;
 val full_name = Name_Space.full_name o naming_of;
 
 fun map_naming f =
-  map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
+  map_bottom (fn (naming, operations, after_close, brittle, target) =>
     (f naming, operations, after_close, brittle, target));
 
 val conceal = map_naming Name_Space.conceal;
@@ -222,7 +222,7 @@
 
 (* target contexts *)
 
-val target_of = #target o get_last_lthy;
+val target_of = #target o bottom_of;
 
 fun target f lthy =
   let
@@ -249,7 +249,7 @@
 
 (** operations **)
 
-val operations_of = #operations o get_first_lthy;
+val operations_of = #operations o top_of;
 
 
 (* primitives *)
@@ -311,7 +311,7 @@
 (* activation of locale fragments *)
 
 fun activate_nonbrittle dep_morph mixin export =
-  map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
+  map_bottom (fn (naming, operations, after_close, brittle, target) =>
     (naming, operations, after_close, brittle,
       (Context.proof_map ooo Locale.add_registration) dep_morph mixin export target));