src/Pure/Isar/isar_syn.ML
changeset 7908 0b191b36ad97
parent 7891 c77ad0c3c92f
child 7931 fa6fec415492
--- 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;