diff --git a/src/HOL/Eisbach/method_closure.ML b/src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML
+++ b/src/HOL/Eisbach/method_closure.ML
@@ -1,251 +1,251 @@
 (*  Title:      HOL/Eisbach/method_closure.ML
     Author:     Daniel Matichuk, NICTA/UNSW
 
 Facilities for treating method syntax as a closure, with abstraction
 over terms, facts and other methods.
 
 The 'method' command allows to define new proof methods by combining
 existing ones with their usual syntax.
 *)
 
 signature METHOD_CLOSURE =
 sig
   val apply_method: Proof.context -> string -> term list -> thm list list ->
     (Proof.context -> Method.method) list -> Proof.context -> thm list -> context_tactic
   val method: binding -> (binding * typ option * mixfix) list -> binding list ->
     binding list -> binding list -> Token.src -> local_theory -> string * local_theory
   val method_cmd: binding -> (binding * string option * mixfix) list -> binding list ->
     binding list -> binding list -> Token.src -> local_theory -> string * local_theory
 end;
 
 structure Method_Closure: METHOD_CLOSURE =
 struct
 
 (* auxiliary data for method definition *)
 
 structure Method_Definition = Proof_Data
 (
   type T =
     (Proof.context -> Method.method) Symtab.table *  (*dynamic methods*)
     (term list -> Proof.context -> Method.method) Symtab.table  (*recursive methods*);
   fun init _ : T = (Symtab.empty, Symtab.empty);
 );
 
 fun lookup_dynamic_method ctxt full_name =
   (case Symtab.lookup (#1 (Method_Definition.get ctxt)) full_name of
     SOME m => m ctxt
   | NONE => error ("Illegal use of internal Eisbach method: " ^ quote full_name));
 
 val update_dynamic_method = Method_Definition.map o apfst o Symtab.update;
 
 fun get_recursive_method full_name ts ctxt =
   (case Symtab.lookup (#2 (Method_Definition.get ctxt)) full_name of
     SOME m => m ts ctxt
   | NONE => error ("Illegal use of internal Eisbach method: " ^ quote full_name));
 
 val put_recursive_method = Method_Definition.map o apsnd o Symtab.update;
 
 
 (* stored method closures *)
 
 type closure = {vars: term list, named_thms: string list, methods: string list, body: Method.text};
 
 structure Data = Generic_Data
 (
   type T = closure Symtab.table;
   val empty: T = Symtab.empty;
   val extend = I;
   fun merge data : T = Symtab.merge (K true) data;
 );
 
 fun get_closure ctxt name =
   (case Symtab.lookup (Data.get (Context.Proof ctxt)) name of
     SOME closure => closure
   | NONE => error ("Unknown Eisbach method: " ^ quote name));
 
 fun put_closure binding (closure: closure) lthy =
   let
     val name = Local_Theory.full_name lthy binding;
   in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
       Data.map
         (Symtab.update (name,
           {vars = map (Morphism.term phi) (#vars closure),
            named_thms = #named_thms closure,
            methods = #methods closure,
            body = (Method.map_source o map) (Token.transform phi) (#body closure)})))
   end;
 
 
 (* instantiate and evaluate method text *)
 
 fun method_instantiate vars body ts ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
     val subst = fold (Pattern.match thy) (vars ~~ ts) (Vartab.empty, Vartab.empty);
     val morphism = Morphism.term_morphism "method_instantiate" (Envir.subst_term subst);
     val body' = (Method.map_source o map) (Token.transform morphism) body;
   in Method.evaluate_runtime body' ctxt end;
 
 
 
 (** apply method closure **)
 
 fun recursive_method full_name vars body ts =
   let val m = method_instantiate vars body
   in put_recursive_method (full_name, m) #> m ts end;
 
 fun apply_method ctxt method_name terms facts methods =
   let
     fun declare_facts (name :: names) (fact :: facts) =
           fold (Context.proof_map o Named_Theorems.add_thm name) fact
           #> declare_facts names facts
       | declare_facts _ [] = I
       | declare_facts [] (_ :: _) = error ("Excessive facts for method " ^ quote method_name);
     val {vars, named_thms, methods = method_args, body} = get_closure ctxt method_name;
   in
     declare_facts named_thms facts
     #> fold update_dynamic_method (method_args ~~ methods)
     #> recursive_method method_name vars body terms
   end;
 
 
 
 (** define method closure **)
 
 local
 
 fun setup_local_method binding lthy =
   let
     val full_name = Local_Theory.full_name lthy binding;
     fun dynamic_method ctxt = lookup_dynamic_method ctxt full_name;
   in
     lthy
     |> update_dynamic_method (full_name, K Method.fail)
     |> Method.local_setup binding (Scan.succeed dynamic_method) "(internal)"
   end;
 
 fun check_named_thm ctxt binding =
   let
     val bname = Binding.name_of binding;
     val pos = Binding.pos_of binding;
     val full_name = Named_Theorems.check ctxt (bname, pos);
     val parser: Method.modifier parser =
       Args.$$$ bname -- Args.colon
         >> K {init = I, attribute = Named_Theorems.add full_name, pos = pos};
   in (full_name, parser) end;
 
 fun parse_term_args args =
   Args.context :|-- (fn ctxt =>
     let
       val ctxt' = Proof_Context.set_mode (Proof_Context.mode_schematic) ctxt;
 
       fun parse T =
         (if T = propT then Syntax.parse_prop ctxt' else Syntax.parse_term ctxt')
         #> Type.constraint (Type_Infer.paramify_vars T);
 
       fun do_parse' T =
         Parse_Tools.name_term >> Parse_Tools.parse_val_cases (parse T);
 
       fun do_parse (Var (_, T)) = do_parse' T
         | do_parse (Free (_, T)) = do_parse' T
         | do_parse t = error ("Unexpected method parameter: " ^ Syntax.string_of_term ctxt' t);
 
        fun rep [] x = Scan.succeed [] x
          | rep (t :: ts) x  = (do_parse t ::: rep ts) x;
 
       fun check ts =
         let
           val (ts, fs) = split_list ts;
           val ts' = Syntax.check_terms ctxt' ts |> Variable.polymorphic ctxt';
           val _ = ListPair.app (fn (f, t) => f t) (fs, ts');
         in ts' end;
     in Scan.lift (rep args) >> check end);
 
 fun parse_method_args method_args =
   let
     fun bind_method (name, text) ctxt =
       let
         val method = Method.evaluate_runtime text;
         val inner_update = method o update_dynamic_method (name, K (method ctxt));
       in update_dynamic_method (name, inner_update) ctxt end;
 
     fun rep [] x = Scan.succeed [] x
       | rep (m :: ms) x = ((Method.text_closure >> pair m) ::: rep ms) x;
   in rep method_args >> fold bind_method end;
 
 fun gen_method add_fixes name vars uses declares methods source lthy =
   let
     val (uses_internal, lthy1) = lthy
       |> Proof_Context.concealed
-      |> Local_Theory.begin_target |-> Proof_Context.private_scope
+      |> Local_Theory.begin_target I |-> Proof_Context.private_scope
       |> Local_Theory.map_background_naming (Name_Space.add_path (Binding.name_of name))
       |> Config.put Method.old_section_parser true
       |> fold setup_local_method methods
       |> fold_map (fn b => Named_Theorems.declare b "") uses;
 
     val (term_args, lthy2) = lthy1
       |> add_fixes vars |-> fold_map Proof_Context.inferred_param |>> map Free;
 
     val (named_thms, modifiers) = map (check_named_thm lthy2) (declares @ uses) |> split_list;
 
     val method_args = map (Local_Theory.full_name lthy2) methods;
 
     fun parser args meth =
       apfst (Config.put_generic Method.old_section_parser true) #>
       (parse_term_args args --
         parse_method_args method_args --|
         (Scan.depend (fn context =>
           Scan.succeed (fold Named_Theorems.clear uses_internal context, ())) --
          Method.sections modifiers)) >> (fn (ts, decl) => meth ts o decl);
 
     val full_name = Local_Theory.full_name lthy name;
 
     val lthy3 = lthy2
       |> Method.local_setup (Binding.make (Binding.name_of name, Position.none))
         (parser term_args (get_recursive_method full_name)) "(internal)"
       |> put_recursive_method (full_name, fn _ => fn _ => Method.fail);
 
     val (text, src) =
       Method.read_closure (Config.put Proof_Context.dynamic_facts_dummy true lthy3) source;
 
     val morphism =
       Variable.export_morphism lthy3
         (lthy
           |> Proof_Context.transfer (Proof_Context.theory_of lthy3)
           |> fold Token.declare_maxidx src
           |> Variable.declare_maxidx (Variable.maxidx_of lthy3));
 
     val text' = (Method.map_source o map) (Token.transform morphism) text;
     val term_args' = map (Morphism.term morphism) term_args;
   in
     lthy3
     |> Local_Theory.close_target
     |> Proof_Context.restore_naming lthy
     |> put_closure name
         {vars = term_args', named_thms = named_thms, methods = method_args, body = text'}
     |> Method.local_setup name
         (Args.context :|-- (fn ctxt =>
           let val {body, vars, ...} = get_closure ctxt full_name in
             parser vars (recursive_method full_name vars body) end)) ""
     |> pair full_name
   end;
 
 in
 
 val method = gen_method Proof_Context.add_fixes;
 val method_cmd = gen_method Proof_Context.add_fixes_cmd;
 
 end;
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>method\<close> "Eisbach method definition"
     (Parse.binding -- Parse.for_fixes --
       ((Scan.optional (\<^keyword>\<open>methods\<close> |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
         (Scan.optional (\<^keyword>\<open>uses\<close> |-- Parse.!!! (Scan.repeat1 Parse.binding)) [])) --
       (Scan.optional (\<^keyword>\<open>declares\<close> |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
       Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.args1 (K true)) >>
       (fn ((((name, vars), (methods, uses)), declares), src) =>
         #2 o method_cmd name vars uses declares methods src));
 
 end;
diff --git a/src/Pure/Isar/bundle.ML b/src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML
+++ b/src/Pure/Isar/bundle.ML
@@ -1,243 +1,241 @@
 (*  Title:      Pure/Isar/bundle.ML
     Author:     Makarius
 
 Bundled declarations (notes etc.).
 *)
 
 signature BUNDLE =
 sig
   val check: Proof.context -> xstring * Position.T -> string
   val get_bundle: Proof.context -> string -> Attrib.thms
   val get_bundle_cmd: Proof.context -> xstring * Position.T -> Attrib.thms
   val print_bundles: bool -> Proof.context -> unit
   val bundle: binding * Attrib.thms ->
     (binding * typ option * mixfix) list -> local_theory -> local_theory
   val bundle_cmd: binding * (Facts.ref * Token.src list) list ->
     (binding * string option * mixfix) list -> local_theory -> local_theory
   val init: binding -> theory -> local_theory
   val unbundle: string list -> local_theory -> local_theory
   val unbundle_cmd: (xstring * Position.T) list -> local_theory -> local_theory
   val includes: string list -> Proof.context -> Proof.context
   val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
   val include_: string list -> Proof.state -> Proof.state
   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 -> Binding.scope * local_theory
   val context_cmd: (xstring * Position.T) list -> Element.context list ->
     generic_theory -> Binding.scope * local_theory
 end;
 
 structure Bundle: BUNDLE =
 struct
 
 (** context data **)
 
 structure Data = Generic_Data
 (
   type T = Attrib.thms Name_Space.table * Attrib.thms option;
   val empty : T = (Name_Space.empty_table "bundle", NONE);
   val extend = I;
   fun merge ((tab1, target1), (tab2, target2)) =
     (Name_Space.merge_tables (tab1, tab2), merge_options (target1, target2));
 );
 
 
 (* bundles *)
 
 val get_bundles_generic = #1 o Data.get;
 val get_bundles = get_bundles_generic o Context.Proof;
 
 fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt);
 
 val get_bundle_generic = Name_Space.get o get_bundles_generic;
 val get_bundle = get_bundle_generic o Context.Proof;
 fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt;
 
 fun define_bundle (b, bundle) context =
   let
     val bundle' = Attrib.trim_context_thms bundle;
     val (name, bundles') = Name_Space.define context true (b, bundle') (get_bundles_generic context);
     val context' = (Data.map o apfst o K) bundles' context;
   in (name, context') end;
 
 
 (* target -- bundle under construction *)
 
 fun the_target thy =
   (case #2 (Data.get (Context.Theory thy)) of
     SOME thms => thms
   | NONE => error "Missing bundle target");
 
 val reset_target = (Context.theory_map o Data.map o apsnd o K) NONE;
 val set_target = Context.theory_map o Data.map o apsnd o K o SOME o Attrib.trim_context_thms;
 
 fun augment_target thms =
   Local_Theory.background_theory (fn thy => set_target (the_target thy @ thms) thy);
 
 
 (* print bundles *)
 
 fun pretty_bundle ctxt (markup_name, bundle) =
   let
     val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
     fun prt_thm_attribs atts th =
       Pretty.block (Pretty.breaks (prt_thm th :: Attrib.pretty_attribs ctxt atts));
     fun prt_thms (ths, []) = map prt_thm ths
       | prt_thms (ths, atts) = map (prt_thm_attribs atts) ths;
   in
     Pretty.block ([Pretty.keyword1 "bundle", Pretty.str " ", Pretty.mark_str markup_name] @
       (if null bundle then [] else Pretty.fbreaks (Pretty.str " =" :: maps prt_thms bundle)))
   end;
 
 fun print_bundles verbose ctxt =
   Pretty.writeln_chunks
     (map (pretty_bundle ctxt) (Name_Space.markup_table verbose ctxt (get_bundles ctxt)));
 
 
 
 (** define bundle **)
 
 fun transform_bundle phi =
   map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts));
 
 
 (* command *)
 
 local
 
 fun gen_bundle prep_fact prep_att add_fixes (binding, raw_bundle) raw_fixes lthy =
   let
     val (_, ctxt') = add_fixes raw_fixes lthy;
     val bundle0 = raw_bundle
       |> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts));
     val bundle =
       Attrib.partial_evaluation ctxt' [(Binding.empty_atts, bundle0)] |> map snd |> flat
       |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);
   in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
       (fn phi => #2 o define_bundle (Morphism.binding phi binding, transform_bundle phi bundle))
   end;
 
 in
 
 val bundle = gen_bundle (K I) (K I) Proof_Context.add_fixes;
 val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.add_fixes_cmd;
 
 end;
 
 
 (* target *)
 
 local
 
 fun bad_operation _ = error "Not possible in bundle target";
 
 fun conclude invisible binding =
   Local_Theory.background_theory_result (fn thy =>
     thy
     |> invisible ? Context_Position.set_visible_global false
     |> Context.Theory
     |> define_bundle (binding, the_target thy)
     ||> (Context.the_theory
       #> invisible ? Context_Position.restore_visible_global thy
       #> reset_target));
 
 fun pretty binding lthy =
   let
     val bundle = the_target (Proof_Context.theory_of lthy);
     val (name, lthy') = lthy
       |> Local_Theory.raw_theory (Context_Position.set_visible_global false)
       |> conclude true binding;
     val thy_ctxt' = Proof_Context.init_global (Proof_Context.theory_of lthy');
     val markup_name =
       Name_Space.markup_extern thy_ctxt' (Name_Space.space_of_table (get_bundles thy_ctxt')) name;
   in [pretty_bundle lthy' (markup_name, bundle)] end;
 
 fun bundle_notes kind facts lthy =
   let
     val bundle = facts
       |> maps (fn ((_, more_atts), thms) => map (fn (ths, atts) => (ths, atts @ more_atts)) thms);
   in
     lthy
     |> augment_target (transform_bundle (Local_Theory.standard_morphism_theory lthy) bundle)
     |> Generic_Target.standard_notes (op <>) kind facts
     |> Attrib.local_notes kind facts
   end;
 
 fun bundle_declaration decl lthy =
   lthy
   |> (augment_target o Attrib.internal_declaration)
     (Morphism.transform (Local_Theory.standard_morphism_theory lthy) decl)
   |> Generic_Target.standard_declaration (K true) decl;
 
 in
 
 fun init binding thy =
   thy
   |> Generic_Target.init
      {background_naming = Sign.naming_of thy,
       setup = set_target [] #> Proof_Context.init_global,
       conclude = conclude false binding #> #2}
      {define = bad_operation,
       notes = bundle_notes,
       abbrev = bad_operation,
       declaration = K bundle_declaration,
       theory_registration = bad_operation,
       locale_dependency = bad_operation,
       pretty = pretty binding}
 
 end;
 
 
 
 (** activate bundles **)
 
 local
 
 fun gen_activate notes get args ctxt =
   let val decls = maps (get ctxt) args in
     ctxt
     |> Context_Position.set_visible false
     |> notes [(Binding.empty_atts, decls)] |> #2
     |> Context_Position.restore_visible ctxt
   end;
 
 fun gen_includes get = gen_activate (Attrib.local_notes "") get;
 
 fun gen_context get prep_decl raw_incls raw_elems gthy =
   let
     val (after_close, lthy) =
       gthy |> Context.cases (pair Local_Theory.exit o Named_Target.theory_init)
         (pair I o Local_Theory.assert);
     val ((_, _, _, lthy'), _) = lthy
       |> gen_includes get raw_incls
       |> prep_decl ([], []) I raw_elems;
   in
-    lthy' |> Local_Theory.init_target
-      {background_naming = Local_Theory.background_naming_of lthy, after_close = after_close}
-      (Local_Theory.operations_of lthy)
+    lthy' |> Local_Theory.begin_target after_close
   end;
 
 in
 
 val unbundle = gen_activate Local_Theory.notes get_bundle;
 val unbundle_cmd = gen_activate Local_Theory.notes get_bundle_cmd;
 
 val includes = gen_includes get_bundle;
 val includes_cmd = gen_includes get_bundle_cmd;
 
 fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts;
 fun include_cmd bs =
   Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.reset_facts;
 
 fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
 fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
 
 val context = gen_context get_bundle Expression.cert_declaration;
 val context_cmd = gen_context get_bundle_cmd Expression.read_declaration;
 
 end;
 
 end;
diff --git a/src/Pure/Isar/local_theory.ML b/src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML
+++ b/src/Pure/Isar/local_theory.ML
@@ -1,418 +1,416 @@
 (*  Title:      Pure/Isar/local_theory.ML
     Author:     Makarius
 
 Local theory operations, with abstract target context.
 *)
 
 type local_theory = Proof.context;
 type generic_theory = Context.generic;
 
 structure Attrib =
 struct
   type binding = binding * Token.src list;
   type thms = (thm list * Token.src list) list;
   type fact = binding * thms;
 end;
 
 structure Locale =
 struct
   type registration = {inst: string * morphism, mixin: (morphism * bool) option, export: morphism};
 end;
 
 signature LOCAL_THEORY =
 sig
   type operations
   val assert: local_theory -> local_theory
   val level: Proof.context -> int
   val assert_bottom: local_theory -> local_theory
   val mark_brittle: local_theory -> local_theory
   val assert_nonbrittle: local_theory -> local_theory
   val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
   val background_naming_of: local_theory -> Name_Space.naming
   val map_background_naming: (Name_Space.naming -> Name_Space.naming) ->
     local_theory -> local_theory
   val restore_background_naming: local_theory -> local_theory -> local_theory
   val full_name: local_theory -> binding -> string
   val new_group: local_theory -> local_theory
   val reset_group: local_theory -> local_theory
   val standard_morphism: local_theory -> Proof.context -> morphism
   val standard_morphism_theory: local_theory -> morphism
   val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
   val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val background_theory: (theory -> theory) -> local_theory -> local_theory
   val target_of: local_theory -> Proof.context
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val target_morphism: local_theory -> morphism
   val propagate_ml_env: generic_theory -> generic_theory
   val operations_of: local_theory -> operations
   val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
   val notes: Attrib.fact list -> local_theory -> (string * thm list) list * local_theory
   val notes_kind: string -> Attrib.fact list -> local_theory ->
     (string * thm list) list * local_theory
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
   val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
   val theory_registration: Locale.registration -> local_theory -> local_theory
   val locale_dependency: Locale.registration -> local_theory -> local_theory
   val pretty: local_theory -> Pretty.T list
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
   val set_defsort: sort -> local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
   val init: {background_naming: Name_Space.naming, exit: local_theory -> Proof.context} ->
     operations -> Proof.context -> local_theory
   val exit: local_theory -> Proof.context
   val exit_global: local_theory -> theory
   val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
   val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
-  val init_target: {background_naming: Name_Space.naming, after_close: local_theory -> local_theory} ->
-    operations -> local_theory -> Binding.scope * local_theory
-  val begin_target: local_theory -> Binding.scope * local_theory
+  val begin_target: (local_theory -> local_theory) -> local_theory -> Binding.scope * local_theory
   val open_target: local_theory -> local_theory
   val close_target: local_theory -> local_theory
   val subtarget: (local_theory -> local_theory) -> local_theory -> local_theory
   val subtarget_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) ->
     local_theory -> 'b * local_theory
 end;
 
 signature PRIVATE_LOCAL_THEORY =
 sig
   include LOCAL_THEORY
   val reset: local_theory -> local_theory
 end
 
 structure Local_Theory: PRIVATE_LOCAL_THEORY =
 struct
 
 (** local theory data **)
 
 (* type lthy *)
 
 type operations =
  {define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory,
   notes: string -> Attrib.fact list -> local_theory -> (string * thm list) list * local_theory,
   abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory,
   declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
   theory_registration: Locale.registration -> local_theory -> local_theory,
   locale_dependency: Locale.registration -> local_theory -> local_theory,
   pretty: local_theory -> Pretty.T list};
 
 type lthy =
  {background_naming: Name_Space.naming,
   operations: operations,
   after_close: local_theory -> local_theory,
   exit: local_theory -> Proof.context,
   brittle: bool,
   target: Proof.context};
 
 fun make_lthy (background_naming, operations, after_close, exit, brittle, target) : lthy =
   {background_naming = background_naming, operations = operations,
     after_close = after_close, exit = exit, brittle = brittle, target = target};
 
 
 (* context data *)
 
 structure Data = Proof_Data
 (
   type T = lthy list;
   fun init _ = [];
 );
 
 
 (* nested structure *)
 
 val level = length o Data.get;  (*1: main target at bottom, >= 2: nested target context*)
 
 fun assert lthy =
   if level lthy = 0 then error "Missing local theory context" else lthy;
 
 fun assert_bottom lthy =
   let
     val _ = assert lthy;
   in
     if level lthy > 1 then error "Not at bottom of local theory nesting"
     else lthy
   end;
 
 fun assert_not_bottom lthy =
   let
     val _ = assert lthy;
   in
     if level lthy = 1 then error "Already at bottom of local theory nesting"
     else lthy
   end;
 
 val bottom_of = List.last o Data.get o assert;
 val top_of = hd o Data.get o assert;
 
 fun map_top f =
   assert #>
   Data.map (fn {background_naming, operations, after_close, exit, brittle, target} :: parents =>
     make_lthy (f (background_naming, operations, after_close, exit, brittle, target)) :: parents);
 
 fun reset lthy = #target (top_of lthy) |> Data.put (Data.get lthy);
 
 fun map_contexts f lthy =
   let val n = level lthy in
     lthy |> (Data.map o map_index)
       (fn (i, {background_naming, operations, after_close, exit, brittle, target}) =>
         make_lthy (background_naming, operations, after_close, exit, brittle,
           target
           |> Context_Position.set_visible false
           |> f (n - i - 1)
           |> Context_Position.restore_visible target))
       |> f n
   end;
 
 
 (* brittle context -- implicit for nested structures *)
 
 fun mark_brittle lthy =
   if level lthy = 1 then
     map_top (fn (background_naming, operations, after_close, exit, _, target) =>
       (background_naming, operations, after_close, exit, true, target)) lthy
   else lthy;
 
 fun assert_nonbrittle lthy =
   if #brittle (top_of lthy) then error "Brittle local theory context"
   else lthy;
 
 
 (* naming for background theory *)
 
 val background_naming_of = #background_naming o top_of;
 
 fun map_background_naming f =
   map_top (fn (background_naming, operations, after_close, exit, brittle, target) =>
     (f background_naming, operations, after_close, exit, brittle, target));
 
 val restore_background_naming = map_background_naming o K o background_naming_of;
 
 val full_name = Name_Space.full_name o background_naming_of;
 
 val new_group = map_background_naming Name_Space.new_group;
 val reset_group = map_background_naming Name_Space.reset_group;
 
 
 (* standard morphisms *)
 
 fun standard_morphism lthy ctxt =
   Proof_Context.norm_export_morphism lthy ctxt $>
   Morphism.binding_morphism "Local_Theory.standard_binding"
     (Name_Space.transform_binding (Proof_Context.naming_of lthy));
 
 fun standard_morphism_theory lthy =
   standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
 
 fun standard_form lthy ctxt x =
   Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
 
 
 (* background theory *)
 
 fun raw_theory_result f lthy =
   let
     val (res, thy') = f (Proof_Context.theory_of lthy);
     val lthy' = map_contexts (K (Proof_Context.transfer thy')) lthy;
   in (res, lthy') end;
 
 fun raw_theory f = #2 o raw_theory_result (f #> pair ());
 
 fun background_theory_result f lthy =
   let
     val naming =
       background_naming_of lthy
       |> Name_Space.transform_naming (Proof_Context.naming_of lthy);
   in
     lthy |> raw_theory_result (fn thy =>
       thy
       |> Sign.map_naming (K naming)
       |> f
       ||> Sign.restore_naming thy)
   end;
 
 fun background_theory f = #2 o background_theory_result (f #> pair ());
 
 
 (* target contexts *)
 
 val target_of = #target o bottom_of;
 
 fun target f lthy =
   let
     val ctxt = target_of lthy;
     val ctxt' = ctxt
       |> Context_Position.set_visible false
       |> f
       |> Context_Position.restore_visible ctxt;
     val thy' = Proof_Context.theory_of ctxt';
   in map_contexts (fn 0 => K ctxt' | _ => Proof_Context.transfer thy') lthy end;
 
 fun target_morphism lthy = standard_morphism lthy (target_of lthy);
 
 fun propagate_ml_env (context as Context.Proof lthy) =
       let val inherit = ML_Env.inherit [context] in
         lthy
         |> background_theory (Context.theory_map inherit)
         |> map_contexts (K (Context.proof_map inherit))
         |> Context.Proof
       end
   | propagate_ml_env context = context;
 
 
 
 (** operations **)
 
 val operations_of = #operations o top_of;
 
 fun operation f lthy = f (operations_of lthy) lthy;
 fun operation2 f x y = operation (fn ops => f ops x y);
 
 
 (* primitives *)
 
 val pretty = operation #pretty;
 val abbrev = operation2 #abbrev;
 val define = operation2 #define false;
 val define_internal = operation2 #define true;
 val notes_kind = operation2 #notes;
 val declaration = operation2 #declaration;
 fun theory_registration registration =
   assert_bottom #> operation (fn ops => #theory_registration ops registration);
 fun locale_dependency registration =
   assert_bottom #> operation (fn ops => #locale_dependency ops registration);
 
 
 (* theorems *)
 
 val notes = notes_kind "";
 fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
 
 fun add_thms_dynamic (binding, f) lthy =
   lthy
   |> background_theory_result (fn thy => thy
       |> Global_Theory.add_thms_dynamic' (Sign.inherit_naming thy lthy) (binding, f))
   |-> (fn name =>
     map_contexts (fn _ => fn ctxt =>
       Proof_Context.transfer_facts (Proof_Context.theory_of ctxt) ctxt) #>
     declaration {syntax = false, pervasive = false} (fn phi =>
       let val binding' = Morphism.binding phi binding in
         Context.mapping
           (Global_Theory.alias_fact binding' name)
           (Proof_Context.alias_fact binding' name)
       end));
 
 
 (* default sort *)
 
 fun set_defsort S =
   declaration {syntax = true, pervasive = false}
     (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
 
 
 (* notation *)
 
 fun type_notation add mode raw_args lthy =
   let
     val args = map (apfst (Logic.type_map (Assumption.export_term lthy (target_of lthy)))) raw_args;
     val args' = map (apsnd Mixfix.reset_pos) args;
     val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.type_notation add mode args;
   in
     declaration {syntax = true, pervasive = false}
       (Proof_Context.generic_type_notation add mode args') lthy
   end;
 
 fun notation add mode raw_args lthy =
   let
     val args = map (apfst (Assumption.export_term lthy (target_of lthy))) raw_args
     val args' = map (apsnd Mixfix.reset_pos) args;
     val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.notation add mode args;
   in
     declaration {syntax = true, pervasive = false}
       (Proof_Context.generic_notation add mode args') lthy
   end;
 
 
 (* name space aliases *)
 
 fun syntax_alias global_alias local_alias b name =
   declaration {syntax = true, pervasive = false} (fn phi =>
     let val b' = Morphism.binding phi b
     in Context.mapping (global_alias b' name) (local_alias b' name) end);
 
 val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias;
 val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias;
 
 
 
 (** manage targets **)
 
 (* main target *)
 
 fun init {background_naming, exit} operations target =
   target |> Data.map
     (fn [] => [make_lthy (background_naming, operations, I, exit, false, target)]
       | _ => error "Local theory already initialized");
 
 val exit_of = #exit o bottom_of;
 
 fun exit lthy = exit_of lthy lthy;
 val exit_global = Proof_Context.theory_of o exit;
 
 fun exit_result decl (x, lthy) =
   let
     val ctxt = exit lthy;
     val phi = standard_morphism lthy ctxt;
   in (decl phi x, ctxt) end;
 
 fun exit_result_global decl (x, lthy) =
   let
     val thy = exit_global lthy;
     val thy_ctxt = Proof_Context.init_global thy;
     val phi = standard_morphism lthy thy_ctxt;
   in (decl phi x, thy) end;
 
 
 (* nested targets *)
 
 fun init_target {background_naming, after_close} operations lthy =
   let
     val _ = assert lthy;
     val after_close' = Proof_Context.restore_naming lthy #> after_close;
     val (scope, target) = Proof_Context.new_scope lthy;
     val entry = make_lthy (background_naming, operations, after_close', exit_of lthy, true, target);
     val lthy' = Data.map (cons entry) target;
   in (scope, lthy') end;
 
-fun begin_target lthy =
-  init_target {background_naming = background_naming_of lthy, after_close = I}
+fun begin_target after_close lthy =
+  init_target {background_naming = background_naming_of lthy, after_close = after_close}
     (operations_of lthy) lthy;
 
-val open_target = begin_target #> #2;
+val open_target = begin_target I #> #2;
 
 fun close_target lthy =
   let
     val _ = assert_not_bottom lthy;
     val ({after_close, ...} :: rest) = Data.get lthy;
   in lthy |> Data.put rest |> reset |> after_close end;
 
 fun subtarget body = open_target #> body #> close_target;
 
 fun subtarget_result decl body lthy =
   let
     val (x, inner_lthy) = lthy |> open_target |> body;
     val lthy' = inner_lthy |> close_target;
     val phi = Proof_Context.export_morphism inner_lthy lthy';
   in (decl phi x, lthy') end;
 
 end;