# HG changeset patch
# User wenzelm
# Date 1119026005 -7200
# Node ID 9b6e6d5fba0597bb7c736c3e42e87f1417a0ba78
# Parent  0509ef1b1ec3f79261722f3a366bcc64d37aa713
Context.theory_name;
tuned;

diff -r 0509ef1b1ec3 -r 9b6e6d5fba05 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Fri Jun 17 18:33:24 2005 +0200
+++ b/src/Pure/proof_general.ML	Fri Jun 17 18:33:25 2005 +0200
@@ -418,10 +418,9 @@
 val update_thy_only = setmp MetaSimplifier.trace_simp 
 			    false ThyInfo.update_thy_only;
 
-fun which_context () =
+fun dynamic_context () =
   (case Context.get_context () of
-    SOME thy => "  Using current (dynamic!) one: " ^
-      (case try PureThy.get_name thy of SOME name => quote name | NONE => "<unnamed>")
+    SOME thy => "  Using current (dynamic!) one: " ^ quote (Context.theory_name thy)
   | NONE => "");
 
 fun try_update_thy_only file =
@@ -429,7 +428,7 @@
     let val name = thy_name file in
       if isSome (ThyLoad.check_file NONE (ThyLoad.thy_path name)) 
       then update_thy_only name
-      else warning ("Unkown theory context of ML file." ^ which_context ())
+      else warning ("Unkown theory context of ML file." ^ dynamic_context ())
     end) ();
 
 
@@ -1164,7 +1163,7 @@
   val fileurl_of = localfile_of_url o (xmlattr "url")
 
   val topthy = Toplevel.theory_of o Toplevel.get_state
-  val topthy_name = PureThy.get_name o topthy
+  val topthy_name = Context.theory_name o topthy
 
   val currently_open_file = ref (NONE : string option)