src/Pure/Isar/bundle.ML
changeset 59890 01aff5aa081d
parent 59880 30687c3f2b10
child 59917 9830c944670f
     1.1 --- a/src/Pure/Isar/bundle.ML	Wed Apr 01 11:55:23 2015 +0200
     1.2 +++ b/src/Pure/Isar/bundle.ML	Wed Apr 01 13:32:32 2015 +0200
     1.3 @@ -20,9 +20,10 @@
     1.4    val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
     1.5    val including: string list -> Proof.state -> Proof.state
     1.6    val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
     1.7 -  val context: string list -> Element.context_i list -> generic_theory -> local_theory
     1.8 +  val context: string list -> Element.context_i list ->
     1.9 +    generic_theory -> Binding.scope * local_theory
    1.10    val context_cmd: (xstring * Position.T) list -> Element.context list ->
    1.11 -    generic_theory -> local_theory
    1.12 +    generic_theory -> Binding.scope * local_theory
    1.13    val print_bundles: Proof.context -> unit
    1.14  end;
    1.15  
    1.16 @@ -97,7 +98,7 @@
    1.17        |> gen_includes get raw_incls
    1.18        |> prep_decl ([], []) I raw_elems;
    1.19    in
    1.20 -    lthy' |> Local_Theory.open_target
    1.21 +    lthy' |> Local_Theory.init_target
    1.22        (Local_Theory.background_naming_of lthy) (Local_Theory.operations_of lthy) after_close
    1.23    end;
    1.24  
    1.25 @@ -137,4 +138,3 @@
    1.26    end |> Pretty.writeln_chunks;
    1.27  
    1.28  end;
    1.29 -