src/Pure/Isar/isar_syn.ML
changeset 27494 0600316f3a3a
parent 27378 0968c0d0b969
child 27525 ee2721e9e900
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Jul 08 17:52:24 2008 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 08 17:52:26 2008 +0200
     1.3 @@ -930,19 +930,18 @@
     1.4  
     1.5  val _ =
     1.6    OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
     1.7 -    (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy));
     1.8 -
     1.9 -val _ =
    1.10 -  OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag
    1.11 -    (P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys));
    1.12 +    (P.name >> (fn name =>
    1.13 +      Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.touch_thy name)));
    1.14  
    1.15  val _ =
    1.16    OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
    1.17 -    (P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy));
    1.18 +    (P.name >> (fn name =>
    1.19 +      Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.remove_thy name)));
    1.20  
    1.21  val _ =
    1.22    OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
    1.23 -    K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy));
    1.24 +    K.diag (P.name >> (fn name =>
    1.25 +      Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.kill_thy name)));
    1.26  
    1.27  val _ =
    1.28    OuterSyntax.improper_command "display_drafts" "display raw source files with symbols"