src/Pure/Isar/toplevel.ML

--- a/src/Pure/Isar/toplevel.ML	Mon Nov 05 20:50:44 2007 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Nov 05 20:50:45 2007 +0100
@@ -114,18 +114,17 @@
 
 type generic_theory = Context.generic;    (*theory or local_theory*)
 
-val loc_init = TheoryTarget.init_cmd;
-
+val loc_init = TheoryTarget.context;
 val loc_exit = ProofContext.theory_of o LocalTheory.exit;
 
-fun loc_begin NONE (Context.Theory thy) = loc_init "-" thy
-  | loc_begin (SOME loc) (Context.Theory thy) = loc_init loc thy
+fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
   | loc_begin NONE (Context.Proof lthy) = lthy
   | loc_begin (SOME loc) (Context.Proof lthy) = loc_init loc (loc_exit lthy);
 
 fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
   | loc_finish NONE (Context.Proof _) = Context.Proof o LocalTheory.restore
-  | loc_finish (SOME _) (Context.Proof lthy) = Context.Proof o LocalTheory.reinit lthy o loc_exit;
+  | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' =>
+      Context.Proof (LocalTheory.reinit (LocalTheory.raw_theory (K (loc_exit lthy')) lthy));
 
 
 (* datatype node *)
@@ -208,7 +207,7 @@
 
 (* print state *)
 
-val pretty_context = LocalTheory.pretty o Context.cases (loc_init "-") I;
+val pretty_context = LocalTheory.pretty o Context.cases (TheoryTarget.init NONE) I;
 
 fun print_state_context state =
   (case try node_of state of