src/Pure/Thy/present.ML
changeset 26433 9c2cdf28ecec
parent 26323 73efc70edeef
child 26957 e3f04fdd994d
     1.1 --- a/src/Pure/Thy/present.ML	Thu Mar 27 14:41:20 2008 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Thu Mar 27 14:41:21 2008 +0100
     1.3 @@ -83,7 +83,7 @@
     1.4  );
     1.5  
     1.6  fun get_info thy =
     1.7 -  if member (op =) [Context.ProtoPureN, Context.PureN, Context.CPureN] (Context.theory_name thy)
     1.8 +  if member (op =) [Context.PureN, Context.CPureN] (Context.theory_name thy)
     1.9    then {name = Context.PureN, session = [], is_local = false}
    1.10    else BrowserInfoData.get thy;
    1.11  
    1.12 @@ -244,7 +244,7 @@
    1.13  val session_info = ref (NONE: session_info option);
    1.14  
    1.15  fun with_session x f = (case ! session_info of NONE => x | SOME info => f info);
    1.16 -fun with_context f = f (Context.theory_name (ML_Context.the_context ()));
    1.17 +fun with_context f = f (Context.theory_name (ML_Context.the_global_context ()));
    1.18  
    1.19  
    1.20