# HG changeset patch
# User wenzelm
# Date 1206558876 -3600
# Node ID 8f66999d03a4ead6f3e59aa4c2da93b380614707
# Parent  441ddf3b8f02be881961e3a37982a448faccc38b
removed obsolete use_thy (cf. isar_syn.ML);

diff -r 441ddf3b8f02 -r 8f66999d03a4 src/Pure/Isar/isar_cmd.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 () =>