--- a/src/Pure/Isar/isar_cmd.ML Thu Jul 19 23:18:50 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Thu Jul 19 23:18:51 2007 +0200
@@ -69,9 +69,7 @@
val cd: Path.T -> Toplevel.transition -> Toplevel.transition
val pwd: Toplevel.transition -> Toplevel.transition
val use_thy: string -> Toplevel.transition -> Toplevel.transition
- val use_thy_only: string -> Toplevel.transition -> Toplevel.transition
val update_thy: string -> Toplevel.transition -> Toplevel.transition
- val update_thy_only: 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
@@ -405,10 +403,7 @@
(* load theory files *)
fun use_thy name = Toplevel.imperative (fn () => ML_Context.save ThyInfo.use_thy name);
-fun use_thy_only name = Toplevel.imperative (fn () => ML_Context.save ThyInfo.use_thy_only name);
fun update_thy name = Toplevel.imperative (fn () => ML_Context.save ThyInfo.update_thy name);
-fun update_thy_only name =
- Toplevel.imperative (fn () => ML_Context.save ThyInfo.update_thy_only name);
(* present draft files *)