--- a/src/Pure/Isar/bundle.ML Wed Apr 01 11:55:23 2015 +0200
+++ b/src/Pure/Isar/bundle.ML Wed Apr 01 13:32:32 2015 +0200
@@ -20,9 +20,10 @@
val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
val including: string list -> Proof.state -> Proof.state
val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
- val context: string list -> Element.context_i list -> generic_theory -> local_theory
+ val context: string list -> Element.context_i list ->
+ generic_theory -> Binding.scope * local_theory
val context_cmd: (xstring * Position.T) list -> Element.context list ->
- generic_theory -> local_theory
+ generic_theory -> Binding.scope * local_theory
val print_bundles: Proof.context -> unit
end;
@@ -97,7 +98,7 @@
|> gen_includes get raw_incls
|> prep_decl ([], []) I raw_elems;
in
- lthy' |> Local_Theory.open_target
+ lthy' |> Local_Theory.init_target
(Local_Theory.background_naming_of lthy) (Local_Theory.operations_of lthy) after_close
end;
@@ -137,4 +138,3 @@
end |> Pretty.writeln_chunks;
end;
-