# HG changeset patch
# User wenzelm
# Date 1163193533 -3600
# Node ID 5f5162f40ac70d1dc65191c5ed106f6d9883d7ce
# Parent  11143b6ad87fd2eeed4c08666064a2d3a8c2f980
removed mapping;
added reinit;

diff -r 11143b6ad87f -r 5f5162f40ac7 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Fri Nov 10 22:18:52 2006 +0100
+++ b/src/Pure/Isar/theory_target.ML	Fri Nov 10 22:18:53 2006 +0100
@@ -11,7 +11,6 @@
   val begin: bstring -> Proof.context -> local_theory
   val init: xstring option -> theory -> local_theory
   val init_i: string option -> theory -> local_theory
-  val mapping: xstring option -> (local_theory -> local_theory) -> theory -> Proof.context * theory
 end;
 
 structure TheoryTarget: THEORY_TARGET =
@@ -201,21 +200,20 @@
   | declaration loc f = I;    (* FIXME *)
 
 
-
 (* init and exit *)
 
-fun begin loc ctxt = ctxt
-  |> Data.put (if loc = "" then NONE else SOME loc)
-  |> LocalTheory.init (SOME (NameSpace.base loc))
-     {pretty = pretty loc,
-      consts = consts loc,
-      axioms = axioms,
-      defs = defs,
-      notes = notes loc,
-      term_syntax = term_syntax loc,
-      declaration = declaration loc,
-      reinit = begin loc,
-      exit = K I};
+fun begin loc =
+  Data.put (if loc = "" then NONE else SOME loc) #>
+  LocalTheory.init (SOME (NameSpace.base loc))
+   {pretty = pretty loc,
+    consts = consts loc,
+    axioms = axioms,
+    defs = defs,
+    notes = notes loc,
+    term_syntax = term_syntax loc,
+    declaration = declaration loc,
+    reinit = fn _ => begin loc o (if loc = "" then ProofContext.init else Locale.init loc),
+    exit = LocalTheory.target_of}
 
 fun init_i NONE thy = begin "" (ProofContext.init thy)
   | init_i (SOME loc) thy = begin loc (Locale.init loc thy);
@@ -223,6 +221,4 @@
 fun init (SOME "-") thy = init_i NONE thy
   | init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;
 
-fun mapping loc f = init loc #> f #> LocalTheory.exit false;
-
 end;