--- a/src/Pure/proof_general.ML Tue Oct 19 22:45:20 2004 +0200
+++ b/src/Pure/proof_general.ML Thu Oct 21 19:21:32 2004 +0200
@@ -1168,8 +1168,11 @@
(* properfilecmd: proper theory-level script commands *)
| "opentheory" => isarscript data
| "theoryitem" => isarscript data
- | "closetheory" => (isarscript data;
- writeln ("Theory "^(topthy_name())^" completed."))
+ | "closetheory" => let
+ val thyname = topthy_name()
+ in (isarscript data;
+ writeln ("Theory "^thyname^" completed."))
+ end
(* improperfilecmd: theory-level commands not in script *)
| "aborttheory" => isarcmd ("init_toplevel")
| "retracttheory" => isarcmd ("kill_thy " ^ (quote (thyname_attr attrs)))