--- 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