src/Pure/context.ML
changeset 37871 c7ce7685e087
parent 37867 b9783e9e96e1
child 39020 ac0f24f850c9
     1.1 --- a/src/Pure/context.ML	Wed Jul 21 15:23:46 2010 +0200
     1.2 +++ b/src/Pure/context.ML	Wed Jul 21 15:31:38 2010 +0200
     1.3 @@ -41,6 +41,7 @@
     1.4    val pretty_abbrev_thy: theory -> Pretty.T
     1.5    val str_of_thy: theory -> string
     1.6    val get_theory: theory -> string -> theory
     1.7 +  val this_theory: theory -> string -> theory
     1.8    val deref: theory_ref -> theory
     1.9    val check_thy: theory -> theory_ref
    1.10    val eq_thy: theory * theory -> bool
    1.11 @@ -253,6 +254,10 @@
    1.12    else if #stage (history_of thy) = finished then thy
    1.13    else error ("Unfinished theory " ^ quote name);
    1.14  
    1.15 +fun this_theory thy name =
    1.16 +  if theory_name thy = name then thy
    1.17 +  else get_theory thy name;
    1.18 +
    1.19  
    1.20  (* theory references *)
    1.21