Fix <closetheory>
authoraspinall
Thu Oct 21 19:21:32 2004 +0200 (2004-10-21)
changeset 152536e20cc79bde6
parent 15252 d4f1b11c336b
child 15254 10cfd6a14682
Fix <closetheory>
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/proof_general.ML	Tue Oct 19 22:45:20 2004 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Thu Oct 21 19:21:32 2004 +0200
     1.3 @@ -1168,8 +1168,11 @@
     1.4       (* properfilecmd: proper theory-level script commands *)
     1.5       | "opentheory"     => isarscript data
     1.6       | "theoryitem"     => isarscript data
     1.7 -     | "closetheory"    => (isarscript data;
     1.8 -			    writeln ("Theory "^(topthy_name())^" completed."))
     1.9 +     | "closetheory"    => let 
    1.10 +			      val thyname = topthy_name()
    1.11 +			   in (isarscript data;
    1.12 +			       writeln ("Theory "^thyname^" completed."))
    1.13 +			   end
    1.14       (* improperfilecmd: theory-level commands not in script *)
    1.15       | "aborttheory"    => isarcmd ("init_toplevel")
    1.16       | "retracttheory"  => isarcmd ("kill_thy " ^ (quote (thyname_attr attrs)))