clarified terminology: first is top (amending d110b0d1bc12);
authorwenzelm
Wed Aug 13 12:59:27 2014 +0200 (2014-08-13)
changeset 579252bd92d3f92d7
parent 57924 a3360da1d2f0
child 57926 59b2572e8e93
clarified terminology: first is top (amending d110b0d1bc12);
src/Pure/Isar/local_theory.ML
     1.1 --- a/src/Pure/Isar/local_theory.ML	Wed Aug 13 12:52:26 2014 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Aug 13 12:59:27 2014 +0200
     1.3 @@ -115,7 +115,7 @@
     1.4  val bottom_of = List.last o Data.get o assert;
     1.5  val top_of = hd o Data.get o assert;
     1.6  
     1.7 -fun map_bottom f =
     1.8 +fun map_top f =
     1.9    assert #>
    1.10    Data.map (fn {naming, operations, after_close, brittle, target} :: parents =>
    1.11      make_lthy (f (naming, operations, after_close, brittle, target)) :: parents);
    1.12 @@ -163,7 +163,7 @@
    1.13  
    1.14  fun mark_brittle lthy =
    1.15    if level lthy = 1 then
    1.16 -    map_bottom (fn (naming, operations, after_close, brittle, target) =>
    1.17 +    map_top (fn (naming, operations, after_close, brittle, target) =>
    1.18        (naming, operations, after_close, true, target)) lthy
    1.19    else lthy;
    1.20  
    1.21 @@ -178,7 +178,7 @@
    1.22  val full_name = Name_Space.full_name o naming_of;
    1.23  
    1.24  fun map_naming f =
    1.25 -  map_bottom (fn (naming, operations, after_close, brittle, target) =>
    1.26 +  map_top (fn (naming, operations, after_close, brittle, target) =>
    1.27      (f naming, operations, after_close, brittle, target));
    1.28  
    1.29  val conceal = map_naming Name_Space.conceal;
    1.30 @@ -310,7 +310,7 @@
    1.31  (* activation of locale fragments *)
    1.32  
    1.33  fun activate_nonbrittle dep_morph mixin export =
    1.34 -  map_bottom (fn (naming, operations, after_close, brittle, target) =>
    1.35 +  map_top (fn (naming, operations, after_close, brittle, target) =>
    1.36      (naming, operations, after_close, brittle,
    1.37        (Context.proof_map ooo Locale.add_registration) dep_morph mixin export target));
    1.38