src/Pure/Isar/toplevel.ML

   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
   val theory': (bool -> theory -> theory) -> transition -> transition
   val theory: (theory -> theory) -> transition -> transition
   val begin_main_target: bool -> (theory -> local_theory) -> transition -> transition
   val end_main_target: transition -> transition
-  val begin_nested_target: (local_theory -> local_theory) -> transition -> transition
+  val begin_nested_target: (Context.generic -> local_theory) -> transition -> transition
   val end_nested_target: transition -> transition
   val local_theory': (bool * Position.T) option -> (xstring * Position.T) option ->
     (bool -> local_theory -> local_theory) -> transition -> transition
   val local_theory: (bool * Position.T) option -> (xstring * Position.T) option ->
     (local_theory -> local_theory) -> transition -> transition

 
 fun begin_main_target begin f = transaction (fn _ =>
   (fn Theory (Context.Theory thy) =>
         let
           val lthy = f thy;
-          val gthy = if begin then Context.Proof lthy else Context.Theory (Named_Target.exit lthy);
+          val gthy =
+            if begin
+            then Context.Proof lthy
+            else Context.Theory (Target_Context.end_named_cmd lthy);
           val _ =
             (case Local_Theory.pretty lthy of
               [] => ()
             | prts => Output.state (Pretty.string_of (Pretty.chunks prts)));
         in (Theory gthy, lthy) end
     | _ => raise UNDEF));
 
 val end_main_target = transaction (fn _ =>
-  (fn Theory (Context.Proof lthy) => (Theory (Context.Theory (Named_Target.exit lthy)), lthy)
+  (fn Theory (Context.Proof lthy) => (Theory (Context.Theory (Target_Context.end_named_cmd lthy)), lthy)
     | _ => raise UNDEF));
 
 fun begin_nested_target f = transaction0 (fn _ =>
   (fn Theory gthy =>
         let
-          val lthy = Bundle.begin_nested_target gthy;
-          val lthy' = f lthy
+          val lthy' = f gthy;
         in Theory (Context.Proof lthy') end
     | _ => raise UNDEF));
 
 val end_nested_target = transaction (fn _ =>
   (fn Theory (Context.Proof lthy) =>
         (case try Local_Theory.end_nested lthy of
           SOME lthy' =>
-            let val gthy' = Bundle.end_nested_target lthy'
+            let val gthy' = Target_Context.end_nested_cmd lthy'
             in (Theory gthy', lthy) end
         | NONE => raise UNDEF)
     | _ => raise UNDEF));
 
 fun restricted_context (SOME (strict, scope)) =

   | restricted_context NONE = I;
 
 fun local_theory' restricted target f = present_transaction (fn int =>
   (fn Theory gthy =>
         let
-          val (finish, lthy) = Named_Target.switch target gthy;
+          val (finish, lthy) = Target_Context.switch_named_cmd target gthy;
           val lthy' = lthy
             |> restricted_context restricted
             |> Local_Theory.new_group
             |> f int
             |> Local_Theory.reset_group;

 
 fun local_theory restricted target f = local_theory' restricted target (K f);
 
 fun present_local_theory target = present_transaction (fn _ =>
   (fn Theory gthy =>
-        let val (finish, lthy) = Named_Target.switch target gthy;
+        let val (finish, lthy) = Target_Context.switch_named_cmd target gthy;
         in (Theory (finish lthy), lthy) end
     | _ => raise UNDEF));
 
 
 (* proof transitions *)

 in
 
 fun local_theory_to_proof' restricted target f = begin_proof
   (fn int => fn gthy =>
     let
-      val (finish, lthy) = Named_Target.switch target gthy;
+      val (finish, lthy) = Target_Context.switch_named_cmd target gthy;
       val prf = lthy
         |> restricted_context restricted
         |> Local_Theory.new_group
         |> f int;
     in (finish o Local_Theory.reset_group, prf) end);

       end;
 
 end;
 
 end;
-
-structure Local_Theory : LOCAL_THEORY = struct open Local_Theory; end;