1.1 --- a/src/Pure/Isar/toplevel.ML	Fri Nov 13 20:41:29 2009 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Nov 13 21:11:15 2009 +0100
     1.3 @@ -105,16 +105,16 @@
     1.4  type generic_theory = Context.generic;    (*theory or local_theory*)
     1.5  
     1.6  val loc_init = Theory_Target.context;
     1.7 -val loc_exit = LocalTheory.exit_global;
     1.8 +val loc_exit = Local_Theory.exit_global;
     1.9  
    1.10  fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
    1.11    | loc_begin NONE (Context.Proof lthy) = lthy
    1.12    | loc_begin (SOME loc) (Context.Proof lthy) = loc_init loc (loc_exit lthy);
    1.13  
    1.14  fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
    1.15 -  | loc_finish NONE (Context.Proof _) = Context.Proof o LocalTheory.restore
    1.16 +  | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore
    1.17    | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' =>
    1.18 -      Context.Proof (LocalTheory.reinit (LocalTheory.raw_theory (K (loc_exit lthy')) lthy));
    1.19 +      Context.Proof (Local_Theory.reinit (Local_Theory.raw_theory (K (loc_exit lthy')) lthy));
    1.20  
    1.21  
    1.22  (* datatype node *)
    1.23 @@ -193,7 +193,7 @@
    1.24  
    1.25  (* print state *)
    1.26  
    1.27 -val pretty_context = LocalTheory.pretty o Context.cases (Theory_Target.init NONE) I;
    1.28 +val pretty_context = Local_Theory.pretty o Context.cases (Theory_Target.init NONE) I;
    1.29  
    1.30  fun print_state_context state =
    1.31    (case try node_of state of
    1.32 @@ -259,7 +259,7 @@
    1.33    | stale_error some = some;
    1.34  
    1.35  fun map_theory f (Theory (gthy, ctxt)) =
    1.36 -      Theory (Context.mapping f (LocalTheory.raw_theory f) gthy, ctxt)
    1.37 +      Theory (Context.mapping f (Local_Theory.raw_theory f) gthy, ctxt)
    1.38    | map_theory _ node = node;
    1.39  
    1.40  in