tuned messages;
authorwenzelm
Fri Nov 22 20:36:57 2013 +0100 (2013-11-22 ago)
changeset 5455939d91cac6e91
parent 54558 31844ca390ad
child 54560 7f36da77130d
tuned messages;
src/Pure/System/session.scala
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/System/session.scala	Fri Nov 22 20:28:49 2013 +0100
     1.2 +++ b/src/Pure/System/session.scala	Fri Nov 22 20:36:57 2013 +0100
     1.3 @@ -240,7 +240,7 @@
     1.4    {
     1.5      val header1 =
     1.6        if (thy_load.loaded_theories(name.theory))
     1.7 -        header.error("Attempt to update loaded theory " + quote(name.theory))
     1.8 +        header.error("Cannot update finished theory " + quote(name.theory))
     1.9        else header
    1.10      (name, Document.Node.Deps(header1))
    1.11    }
     2.1 --- a/src/Pure/Thy/thy_info.ML	Fri Nov 22 20:28:49 2013 +0100
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Nov 22 20:36:57 2013 +0100
     2.3 @@ -140,7 +140,7 @@
     2.4  (* main loader actions *)
     2.5  
     2.6  fun remove_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
     2.7 -  if is_finished name then error (loader_msg "attempt to change finished theory" [name])
     2.8 +  if is_finished name then error (loader_msg "cannot update finished theory" [name])
     2.9    else
    2.10      let
    2.11        val succs = thy_graph String_Graph.all_succs [name];