# HG changeset patch
# User wenzelm
# Date 1186510790 -7200
# Node ID 59a5ffec7078b9211ad125e76744b61526b8d50e
# Parent  4ba00a972eb83dc90f14fda2fac7d01d470d6979
theory loader: removed obsolete update_thy (coincides with use_thy);

diff -r 4ba00a972eb8 -r 59a5ffec7078 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Aug 07 20:19:49 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Aug 07 20:19:50 2007 +0200
@@ -69,7 +69,6 @@
   val cd: Path.T -> Toplevel.transition -> Toplevel.transition
   val pwd: Toplevel.transition -> Toplevel.transition
   val use_thy: string -> Toplevel.transition -> Toplevel.transition
-  val update_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
@@ -401,7 +400,6 @@
 (* load theory files *)
 
 fun use_thy name = Toplevel.imperative (fn () => ML_Context.save ThyInfo.use_thy name);
-fun update_thy name = Toplevel.imperative (fn () => ML_Context.save ThyInfo.update_thy name);
 
 
 (* present draft files *)
diff -r 4ba00a972eb8 -r 59a5ffec7078 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Aug 07 20:19:49 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Aug 07 20:19:50 2007 +0200
@@ -901,10 +901,6 @@
   OuterSyntax.improper_command "use_thy" "use theory file" K.diag
     (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy));
 
-val update_thyP =
-  OuterSyntax.improper_command "update_thy" "update theory file" K.diag
-    (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy));
-
 val touch_thyP =
   OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
     (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy));
@@ -1023,9 +1019,9 @@
   print_full_prfsP, print_propP, print_termP, print_typeP,
   print_codesetupP,
   (*system commands*)
-  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];
+  cdP, pwdP, use_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;
diff -r 4ba00a972eb8 -r 59a5ffec7078 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Tue Aug 07 20:19:49 2007 +0200
+++ b/src/Pure/pure_setup.ML	Tue Aug 07 20:19:50 2007 +0200
@@ -8,11 +8,10 @@
 (* ML toplevel use commands *)
 
 fun use name          = Toplevel.program (fn () => ThyInfo.use name);
-fun time_use name     = Toplevel.program (fn () => ThyInfo.time_use name);
 fun use_thys name     = Toplevel.program (fn () => ThyInfo.use_thys name);
 fun use_thy name      = Toplevel.program (fn () => ThyInfo.use_thy name);
+fun time_use name     = Toplevel.program (fn () => ThyInfo.time_use name);
 fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
-fun update_thy name   = Toplevel.program (fn () => ThyInfo.update_thy name);
 
 
 (* the Pure theories *)