Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
LocalTheory.restore;
authorwenzelm
Thu, 09 Nov 2006 21:44:35 +0100
changeset 21277 ac2d7e03a3b1
parent 21276 2285cf5a7560
child 21278 9442e9d75ada
LocalTheory.restore;
src/Pure/Isar/toplevel.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle