src/Pure/Isar/toplevel.ML
changeset 38350 480b2de9927c
parent 38236 d8c7be27e01d
child 38351 ea1ee55aa41f
child 38380 cf42d8355844
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Aug 11 14:41:16 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Aug 11 14:45:38 2010 +0200
     1.3 @@ -103,7 +103,7 @@
     1.4  
     1.5  (* local theory wrappers *)
     1.6  
     1.7 -val loc_init = Theory_Target.context_cmd;
     1.8 +val loc_init = Named_Target.context_cmd;
     1.9  val loc_exit = Local_Theory.exit_global;
    1.10  
    1.11  fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
    1.12 @@ -194,7 +194,7 @@
    1.13  
    1.14  (* print state *)
    1.15  
    1.16 -val pretty_context = Local_Theory.pretty o Context.cases (Theory_Target.init NONE) I;
    1.17 +val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.init NONE) I;
    1.18  
    1.19  fun print_state_context state =
    1.20    (case try node_of state of