# 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 () =>