theory loader: removed obsolete update_thy (coincides with use_thy);
authorwenzelm
Tue Aug 07 20:19:50 2007 +0200 (2007-08-07 ago)
changeset 2417459a5ffec7078
parent 24173 4ba00a972eb8
child 24175 38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/pure_setup.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Aug 07 20:19:49 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Aug 07 20:19:50 2007 +0200
     1.3 @@ -69,7 +69,6 @@
     1.4    val cd: Path.T -> Toplevel.transition -> Toplevel.transition
     1.5    val pwd: Toplevel.transition -> Toplevel.transition
     1.6    val use_thy: string -> Toplevel.transition -> Toplevel.transition
     1.7 -  val update_thy: string -> Toplevel.transition -> Toplevel.transition
     1.8    val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
     1.9    val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
    1.10    val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
    1.11 @@ -401,7 +400,6 @@
    1.12  (* load theory files *)
    1.13  
    1.14  fun use_thy name = Toplevel.imperative (fn () => ML_Context.save ThyInfo.use_thy name);
    1.15 -fun update_thy name = Toplevel.imperative (fn () => ML_Context.save ThyInfo.update_thy name);
    1.16  
    1.17  
    1.18  (* present draft files *)
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Aug 07 20:19:49 2007 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Aug 07 20:19:50 2007 +0200
     2.3 @@ -901,10 +901,6 @@
     2.4    OuterSyntax.improper_command "use_thy" "use theory file" K.diag
     2.5      (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy));
     2.6  
     2.7 -val update_thyP =
     2.8 -  OuterSyntax.improper_command "update_thy" "update theory file" K.diag
     2.9 -    (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy));
    2.10 -
    2.11  val touch_thyP =
    2.12    OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
    2.13      (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy));
    2.14 @@ -1023,9 +1019,9 @@
    2.15    print_full_prfsP, print_propP, print_termP, print_typeP,
    2.16    print_codesetupP,
    2.17    (*system commands*)
    2.18 -  cdP, pwdP, use_thyP, update_thyP, touch_thyP, touch_all_thysP,
    2.19 -  touch_child_thysP, remove_thyP, kill_thyP, display_draftsP,
    2.20 -  print_draftsP, prP, disable_prP, enable_prP, commitP, quitP, exitP,
    2.21 -  init_toplevelP, welcomeP];
    2.22 +  cdP, pwdP, use_thyP, touch_thyP, touch_all_thysP, touch_child_thysP,
    2.23 +  remove_thyP, kill_thyP, display_draftsP, print_draftsP, prP,
    2.24 +  disable_prP, enable_prP, commitP, quitP, exitP, init_toplevelP,
    2.25 +  welcomeP];
    2.26  
    2.27  end;
     3.1 --- a/src/Pure/pure_setup.ML	Tue Aug 07 20:19:49 2007 +0200
     3.2 +++ b/src/Pure/pure_setup.ML	Tue Aug 07 20:19:50 2007 +0200
     3.3 @@ -8,11 +8,10 @@
     3.4  (* ML toplevel use commands *)
     3.5  
     3.6  fun use name          = Toplevel.program (fn () => ThyInfo.use name);
     3.7 -fun time_use name     = Toplevel.program (fn () => ThyInfo.time_use name);
     3.8  fun use_thys name     = Toplevel.program (fn () => ThyInfo.use_thys name);
     3.9  fun use_thy name      = Toplevel.program (fn () => ThyInfo.use_thy name);
    3.10 +fun time_use name     = Toplevel.program (fn () => ThyInfo.time_use name);
    3.11  fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
    3.12 -fun update_thy name   = Toplevel.program (fn () => ThyInfo.update_thy name);
    3.13  
    3.14  
    3.15  (* the Pure theories *)