# HG changeset patch
# User wenzelm
# Date 1184879931 -7200
# Node ID 3ea92c014a3e3231919bc3f4645abf02aaff7bc6
# Parent  365682a666da8155a2bcfb5c2a33d2b087af9532
removed obsolete use/update_thy_only;

diff -r 365682a666da -r 3ea92c014a3e src/Pure/Isar/isar_cmd.ML
--- 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 *)
diff -r 365682a666da -r 3ea92c014a3e src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Jul 19 23:18:50 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 19 23:18:51 2007 +0200
@@ -897,18 +897,10 @@
   OuterSyntax.improper_command "use_thy" "use theory file" K.diag
     (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy));
 
-val use_thy_onlyP =
-  OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML"
-    K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy_only));
-
 val update_thyP =
   OuterSyntax.improper_command "update_thy" "update theory file" K.diag
     (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy));
 
-val update_thy_onlyP =
-  OuterSyntax.improper_command "update_thy_only" "update theory file, ignoring associated ML"
-    K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy_only));
-
 val touch_thyP =
   OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
     (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy));
@@ -1026,9 +1018,9 @@
   print_thmsP, print_prfsP, print_full_prfsP, print_propP,
   print_termP, print_typeP, print_codesetupP,
   (*system commands*)
-  cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
-  touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,
-  kill_thyP, display_draftsP, print_draftsP, prP, disable_prP,
-  enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
+  cdP, pwdP, use_thyP, update_thyP, touch_thyP, touch_all_thysP,
+  touch_child_thysP, remove_thyP, kill_thyP, display_draftsP,
+  print_draftsP, prP, disable_prP, enable_prP, commitP, quitP, exitP,
+  init_toplevelP, welcomeP];
 
 end;