1.1 --- a/src/Pure/Isar/local_theory.ML	Wed Mar 21 17:16:39 2012 +0100
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Mar 21 17:25:35 2012 +0100
     1.3 @@ -10,9 +10,10 @@
     1.4  signature LOCAL_THEORY =
     1.5  sig
     1.6    type operations
     1.7 +  val map_contexts: (Proof.context -> Proof.context) -> local_theory -> local_theory
     1.8 +  val assert: local_theory -> local_theory
     1.9    val level: Proof.context -> int
    1.10 -  val affirm: local_theory -> local_theory
    1.11 -  val map_contexts: (Proof.context -> Proof.context) -> local_theory -> local_theory
    1.12 +  val assert_bottom: bool -> local_theory -> local_theory
    1.13    val open_target: Name_Space.naming -> operations -> local_theory -> local_theory
    1.14    val close_target: local_theory -> local_theory
    1.15    val naming_of: local_theory -> Name_Space.naming
    1.16 @@ -33,6 +34,7 @@
    1.17    val standard_morphism: local_theory -> Proof.context -> morphism
    1.18    val target_morphism: local_theory -> morphism
    1.19    val global_morphism: local_theory -> morphism
    1.20 +  val operations_of: local_theory -> operations
    1.21    val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    1.22      (term * (string * thm)) * local_theory
    1.23    val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    1.24 @@ -96,31 +98,39 @@
    1.25    fun init _ = [];
    1.26  );
    1.27  
    1.28 -val level = length o Data.get;
    1.29 -
    1.30 -fun affirm lthy =
    1.31 -  if level lthy > 0 then lthy
    1.32 -  else error "Missing local theory context";
    1.33 -
    1.34 -val get_lthy = hd o Data.get o affirm;
    1.35 -
    1.36 -fun map_lthy f = affirm #>
    1.37 -  Data.map (fn {naming, operations, target} :: parents =>
    1.38 -    make_lthy (f (naming, operations, target)) :: parents);
    1.39 -
    1.40  fun map_contexts f =
    1.41    (Data.map o map) (fn {naming, operations, target} => make_lthy (naming, operations, f target))
    1.42    #> f;
    1.43  
    1.44 +fun assert lthy =
    1.45 +  if null (Data.get lthy) then error "Missing local theory context" else lthy;
    1.46 +
    1.47 +val get_lthy = hd o Data.get o assert;
    1.48 +
    1.49 +fun map_lthy f = assert #>
    1.50 +  Data.map (fn {naming, operations, target} :: parents =>
    1.51 +    make_lthy (f (naming, operations, target)) :: parents);
    1.52 +
    1.53  
    1.54  (* nested structure *)
    1.55  
    1.56 -fun open_target naming operations target = affirm target
    1.57 +val level = length o Data.get;
    1.58 +
    1.59 +fun assert_bottom b lthy =
    1.60 +  let
    1.61 +    val _ = assert lthy;
    1.62 +    val b' = level lthy <= 1;
    1.63 +  in
    1.64 +    if b andalso not b' then error "Not at bottom of local theory nesting"
    1.65 +    else if not b andalso b' then error "Already at bottom of local theory nesting"
    1.66 +    else lthy
    1.67 +  end;
    1.68 +
    1.69 +fun open_target naming operations target = assert target
    1.70    |> Data.map (cons (make_lthy (naming, operations, target)));
    1.71  
    1.72  fun close_target lthy =
    1.73 -  if level lthy >= 2 then Data.map tl lthy
    1.74 -  else error "Unbalanced local theory targets";
    1.75 +  assert_bottom false lthy |> Data.map tl;
    1.76  
    1.77  
    1.78  (* naming *)
    1.79 @@ -205,9 +215,12 @@
    1.80  
    1.81  (** operations **)
    1.82  
    1.83 +val operations_of = #operations o get_lthy;
    1.84 +
    1.85 +
    1.86  (* primitives *)
    1.87  
    1.88 -fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
    1.89 +fun operation f lthy = f (operations_of lthy) lthy;
    1.90  fun operation2 f x y = operation (fn ops => f ops x y);
    1.91  
    1.92  val pretty = operation #pretty;