# HG changeset patch
# User wenzelm
# Date 1139255995 -3600
# Node ID fa71f2ddd2e8e988e20d39bcbac77093c3298d16
# Parent  ab48b6ac9327b0507e464ce72e0fecf12d7c2248
added local_theory, with optional locale xname;

diff -r ab48b6ac9327 -r fa71f2ddd2e8 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Feb 06 20:59:54 2006 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Feb 06 20:59:55 2006 +0100
@@ -73,6 +73,7 @@
   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
@@ -294,7 +295,7 @@
           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;
 
@@ -456,6 +457,8 @@
 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