exit: pass interactive flag, toplevel result convention;

--- a/src/Pure/Isar/local_theory.ML	Wed Oct 11 22:55:17 2006 +0200
+++ b/src/Pure/Isar/local_theory.ML	Wed Oct 11 22:55:18 2006 +0200
@@ -36,7 +36,7 @@
   val abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> local_theory -> local_theory
   val init: string option -> operations -> Proof.context -> local_theory
   val reinit: local_theory -> local_theory
-  val exit: local_theory -> Proof.context
+  val exit: bool -> local_theory -> Proof.context * theory
 end;
 
 structure LocalTheory: LOCAL_THEORY =
@@ -58,7 +58,7 @@
     (bstring * thm list) list * local_theory,
   term_syntax: (Context.generic -> Context.generic) -> local_theory -> local_theory,
   declaration: (Context.generic -> Context.generic) -> local_theory -> local_theory,
-  exit: local_theory -> local_theory};
+  exit: bool -> local_theory -> local_theory};
 
 datatype lthy = LThy of
  {theory_prefix: string option,
@@ -169,6 +169,8 @@
   let val {theory_prefix, operations, target} = get_lthy lthy
   in init theory_prefix operations target end;
 
-fun exit lthy = lthy |> operation #exit |> target_of;
+fun exit int lthy = lthy
+  |> operation1 #exit int |> target_of
+  |> (fn ctxt => (ctxt, ProofContext.theory_of ctxt));
 
 end;