src/Pure/Isar/isar_syn.ML
changeset 24314 665b3ab2dabe
parent 24219 e558fe311376
child 24423 ae9cd0e92423
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Aug 17 23:10:45 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Aug 17 23:10:46 2007 +0200
     1.3 @@ -905,10 +905,6 @@
     1.4    OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
     1.5      (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy));
     1.6  
     1.7 -val touch_all_thysP =
     1.8 -  OuterSyntax.improper_command "touch_all_thys" "outdate all non-finished theories" K.diag
     1.9 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.touch_all_thys));
    1.10 -
    1.11  val touch_child_thysP =
    1.12    OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag
    1.13      (P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys));
    1.14 @@ -1019,9 +1015,8 @@
    1.15    print_full_prfsP, print_propP, print_termP, print_typeP,
    1.16    print_codesetupP,
    1.17    (*system commands*)
    1.18 -  cdP, pwdP, use_thyP, touch_thyP, touch_all_thysP, touch_child_thysP,
    1.19 -  remove_thyP, kill_thyP, display_draftsP, print_draftsP, prP,
    1.20 -  disable_prP, enable_prP, commitP, quitP, exitP, init_toplevelP,
    1.21 -  welcomeP];
    1.22 +  cdP, pwdP, use_thyP, touch_thyP, touch_child_thysP, remove_thyP,
    1.23 +  kill_thyP, display_draftsP, print_draftsP, prP, disable_prP,
    1.24 +  enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
    1.25  
    1.26  end;