# HG changeset patch
# User wenzelm
# Date 1187385046 -7200
# Node ID 665b3ab2dabe37304cf9c6a76fdb2175aafa8270
# Parent  5a6342236a32a3c853f4133ff3563d697df7536b
removed obsolete touch_all_thys;

diff -r 5a6342236a32 -r 665b3ab2dabe src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Aug 17 23:10:45 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Aug 17 23:10:46 2007 +0200
@@ -46,7 +46,6 @@
   val exit: Toplevel.transition -> Toplevel.transition
   val quit: Toplevel.transition -> Toplevel.transition
   val touch_child_thys: string -> Toplevel.transition -> Toplevel.transition
-  val touch_all_thys: Toplevel.transition -> Toplevel.transition
   val touch_thy: string -> Toplevel.transition -> Toplevel.transition
   val remove_thy: string -> Toplevel.transition -> Toplevel.transition
   val kill_thy: string -> Toplevel.transition -> Toplevel.transition
@@ -323,7 +322,6 @@
 (* touch theories *)
 
 fun touch_child_thys name = Toplevel.imperative (fn () => ThyInfo.touch_child_thys name);
-val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys;
 fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name);
 fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name);
 fun kill_thy name = Toplevel.imperative (fn () => kill_theory name);
diff -r 5a6342236a32 -r 665b3ab2dabe src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Aug 17 23:10:45 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Aug 17 23:10:46 2007 +0200
@@ -905,10 +905,6 @@
   OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
     (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy));
 
-val touch_all_thysP =
-  OuterSyntax.improper_command "touch_all_thys" "outdate all non-finished theories" K.diag
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.touch_all_thys));
-
 val touch_child_thysP =
   OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag
     (P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys));
@@ -1019,9 +1015,8 @@
   print_full_prfsP, print_propP, print_termP, print_typeP,
   print_codesetupP,
   (*system commands*)
-  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];
+  cdP, pwdP, use_thyP, touch_thyP, 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 5a6342236a32 -r 665b3ab2dabe src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Aug 17 23:10:45 2007 +0200
+++ b/src/Pure/Thy/thy_info.ML	Fri Aug 17 23:10:46 2007 +0200
@@ -30,7 +30,6 @@
   val get_parents: string -> string list
   val pretty_theory: theory -> Pretty.T
   val touch_child_thys: string -> unit
-  val touch_all_thys: unit -> unit
   val load_file: bool -> Path.T -> unit
   val use: string -> unit
   val time_use: string -> unit
@@ -254,8 +253,6 @@
 fun touch_thy name = touch_thys [name];
 fun touch_child_thys name = touch_thys (thy_graph Graph.imm_succs name);
 
-fun touch_all_thys () = List.app outdate_thy (get_names ());
-
 end;