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"