# HG changeset patch
# User wenzelm
# Date 1280262212 -7200
# Node ID 0f21ebea4a73d78edf8a0e93a3dd6a0d4adb408e
# Parent  548f3f165d055c8a41b236c9ed4ffa439e19c166
tuned messages and comments;

diff -r 548f3f165d05 -r 0f21ebea4a73 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Jul 27 22:15:51 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Jul 27 22:23:32 2010 +0200
@@ -200,7 +200,7 @@
 (* remove theory *)
 
 fun remove_thy name =
-  if is_finished name then error (loader_msg "cannot change finished theory" [name])
+  if is_finished name then error (loader_msg "attempt to change finished theory" [name])
   else
     let
       val succs = thy_graph Graph.all_succs [name];
@@ -376,7 +376,7 @@
 end;
 
 
-(* use_thy etc. *)
+(* use_thy *)
 
 fun use_thys_dir dir arg =
   schedule_tasks (snd (require_thys [] dir arg Graph.empty));
@@ -385,7 +385,7 @@
 val use_thy = use_thys o single;
 
 
-(* begin theory *)
+(* toplevel begin theory -- without maintaining database *)
 
 fun toplevel_begin_theory name imports uses =
   let