# HG changeset patch
# User wenzelm
# Date 940525141 -7200
# Node ID 0b191b36ad9724c8bf263189eb97d18c37066d50
# Parent  258f136864db20adc9185352a31829b8107c21d7
added touch_child_thys;

diff -r 258f136864db -r 0b191b36ad97 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Oct 21 18:47:33 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Oct 21 18:59:01 1999 +0200
@@ -11,6 +11,7 @@
   val init_toplevel: Toplevel.transition -> Toplevel.transition
   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
@@ -66,6 +67,7 @@
 
 (* 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);
diff -r 258f136864db -r 0b191b36ad97 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Oct 21 18:47:33 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 21 18:59:01 1999 +0200
@@ -554,6 +554,10 @@
   OuterSyntax.improper_command "touch_all_thys" "outdate all non-finished theories" K.diag
     (Scan.succeed IsarCmd.touch_all_thys);
 
+val touch_child_thysP =
+  OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag
+    (P.name >> IsarCmd.touch_child_thys);
+
 val remove_thyP =
   OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
     (P.name >> IsarCmd.remove_thy);
@@ -632,8 +636,9 @@
   print_propP, print_termP, print_typeP,
   (*system commands*)
   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
-  touch_thyP, touch_all_thysP, remove_thyP, prP, disable_prP,
-  enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
+  touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP, prP,
+  disable_prP, enable_prP, commitP, quitP, exitP, init_toplevelP,
+  welcomeP];
 
 
 end;