# HG changeset patch
# User aspinall
# Date 1098379292 -7200
# Node ID 6e20cc79bde68b6cf8f27d2071622981a52faed0
# Parent  d4f1b11c336b1862bab2de04620442f738c31e7d
Fix <closetheory>

diff -r d4f1b11c336b -r 6e20cc79bde6 src/Pure/proof_general.ML
--- 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)))