removed obsolete use_thy (cf. isar_syn.ML);

--- a/src/Pure/Isar/isar_cmd.ML	Wed Mar 26 12:12:52 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 26 20:14:36 2008 +0100
@@ -69,7 +69,6 @@
   val nested_command: Markup.property list -> string * Position.T -> Toplevel.transition
   val cd: Path.T -> Toplevel.transition -> Toplevel.transition
   val pwd: Toplevel.transition -> Toplevel.transition
-  val use_thy: string -> Toplevel.transition -> Toplevel.transition
   val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
   val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
   val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
@@ -410,11 +409,6 @@
 val pwd = Toplevel.imperative (fn () => writeln (Path.implode (File.pwd ())));
 
 
-(* load theory files *)
-
-fun use_thy name = Toplevel.imperative (fn () => ML_Context.save ThyInfo.use_thy name);
-
-
 (* present draft files *)
 
 fun display_drafts files = Toplevel.imperative (fn () =>