# HG changeset patch
# User wenzelm
# Date 1163105075 -3600
# Node ID ac2d7e03a3b1b46e09375b224e0010a219b67b49
# Parent  2285cf5a7560e387c97ed9cd3c6f0e5cb6c6401e
LocalTheory.restore;

diff -r 2285cf5a7560 -r ac2d7e03a3b1 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Nov 09 21:44:34 2006 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Nov 09 21:44:35 2006 +0100
@@ -544,7 +544,7 @@
         in Theory (Context.Theory thy', SOME ctxt') end
     | Theory (Context.Proof lthy, _) =>
         let val (ctxt', lthy') =
-          if is_none loc then f lthy |> (fn lthy' => (lthy', LocalTheory.reinit lthy'))
+          if is_none loc then f lthy |> (fn lthy' => (lthy', LocalTheory.restore lthy'))
           else lthy |> LocalTheory.raw_theory_result (TheoryTarget.mapping loc f)
         in Theory (Context.Proof lthy', SOME ctxt') end
     | _ => raise UNDEF) #> tap (g int));
@@ -578,7 +578,7 @@
   | _ => raise UNDEF));
 
 val global_finish = Context.Theory o ProofContext.theory_of;
-val local_finish = Context.Proof o LocalTheory.reinit;
+val local_finish = Context.Proof o LocalTheory.restore;
 
 fun mixed_finish (Context.Theory _) ctxt = global_finish ctxt
   | mixed_finish (Context.Proof lthy) ctxt =