src/Pure/Isar/toplevel.ML

   val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit)
     -> transition -> transition
   val theory: (theory -> theory) -> transition -> transition
   val theory': (bool -> theory -> theory) -> transition -> transition
   val theory_context: (theory -> Proof.context * theory) -> transition -> transition
+  val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
   val theory_to_proof: (theory -> Proof.state) -> transition -> transition
   val proof: (Proof.state -> Proof.state) -> transition -> transition
   val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
   val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
   val proofs': (bool -> Proof.state -> Proof.state Seq.seq) -> transition -> transition

               |> setmp Output.do_toplevel_errors false)
           |> normal_state
           handle exn => error_state cont_node exn;
       in
         if is_stale result
-        then return (error_state back_node (if_none err stale_theory))
+        then return (error_state back_node (the_default stale_theory err))
         else return (result, err)
       end;
 
 fun mapping f (State (SOME (node, term))) = State (SOME (History.map f node, term))
   | mapping _ state = state;

 fun theory' f = app_current (fn int =>
   (fn Theory (thy, _) => Theory (f int thy, NONE) | _ => raise UNDEF));
 
 fun theory_context f = app_current
   (K (fn Theory (thy, _) => Theory (swap (apfst SOME (f thy))) | _ => raise UNDEF));
+
+fun local_theory loc f = theory_context (LocalTheory.init loc #> f #> LocalTheory.exit);
 
 fun theory_to_proof f = app_current (fn int =>
   (fn Theory (thy, _) =>
     if ! skip_proofs then
       SkipProof ((History.init (undo_limit int) 0, #2 (Proof.global_skip_proof int (f thy))), thy)