src/Pure/proof_general.ML
changeset 16440 9b6e6d5fba05
parent 16259 aed1a8ae4b23
child 16486 1a12cdb6ee6b
     1.1 --- a/src/Pure/proof_general.ML	Fri Jun 17 18:33:24 2005 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Fri Jun 17 18:33:25 2005 +0200
     1.3 @@ -418,10 +418,9 @@
     1.4  val update_thy_only = setmp MetaSimplifier.trace_simp 
     1.5  			    false ThyInfo.update_thy_only;
     1.6  
     1.7 -fun which_context () =
     1.8 +fun dynamic_context () =
     1.9    (case Context.get_context () of
    1.10 -    SOME thy => "  Using current (dynamic!) one: " ^
    1.11 -      (case try PureThy.get_name thy of SOME name => quote name | NONE => "<unnamed>")
    1.12 +    SOME thy => "  Using current (dynamic!) one: " ^ quote (Context.theory_name thy)
    1.13    | NONE => "");
    1.14  
    1.15  fun try_update_thy_only file =
    1.16 @@ -429,7 +428,7 @@
    1.17      let val name = thy_name file in
    1.18        if isSome (ThyLoad.check_file NONE (ThyLoad.thy_path name)) 
    1.19        then update_thy_only name
    1.20 -      else warning ("Unkown theory context of ML file." ^ which_context ())
    1.21 +      else warning ("Unkown theory context of ML file." ^ dynamic_context ())
    1.22      end) ();
    1.23  
    1.24  
    1.25 @@ -1164,7 +1163,7 @@
    1.26    val fileurl_of = localfile_of_url o (xmlattr "url")
    1.27  
    1.28    val topthy = Toplevel.theory_of o Toplevel.get_state
    1.29 -  val topthy_name = PureThy.get_name o topthy
    1.30 +  val topthy_name = Context.theory_name o topthy
    1.31  
    1.32    val currently_open_file = ref (NONE : string option)
    1.33