--- a/src/Pure/Isar/toplevel.ML Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Aug 11 14:45:38 2010 +0200
@@ -103,7 +103,7 @@
(* local theory wrappers *)
-val loc_init = Theory_Target.context_cmd;
+val loc_init = Named_Target.context_cmd;
val loc_exit = Local_Theory.exit_global;
fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
@@ -194,7 +194,7 @@
(* print state *)
-val pretty_context = Local_Theory.pretty o Context.cases (Theory_Target.init NONE) I;
+val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.init NONE) I;
fun print_state_context state =
(case try node_of state of