# HG changeset patch
# User wenzelm
# Date 1215532346 -7200
# Node ID 0600316f3a3aba830b1fe8b42854f6c8b87c8010
# Parent  f05b6944319ce7b02bddcb279796863e8abb8c8b
removed obsolete touch_child_thys;
simplified touch_thy, remove_thy, kill_thy -- inlined;

diff -r f05b6944319c -r 0600316f3a3a src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jul 08 17:52:24 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 08 17:52:26 2008 +0200
@@ -930,19 +930,18 @@
 
 val _ =
   OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
-    (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy));
-
-val _ =
-  OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag
-    (P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys));
+    (P.name >> (fn name =>
+      Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.touch_thy name)));
 
 val _ =
   OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
-    (P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy));
+    (P.name >> (fn name =>
+      Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.remove_thy name)));
 
 val _ =
   OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
-    K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy));
+    K.diag (P.name >> (fn name =>
+      Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.kill_thy name)));
 
 val _ =
   OuterSyntax.improper_command "display_drafts" "display raw source files with symbols"