# HG changeset patch
# User wenzelm
# Date 1279719098 -7200
# Node ID c7ce7685e087d53ab879c2302557d967034f3fb1
# Parent  dd9cfc512b7f9ca58d499385d48cf66e7e01ce81
replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;

diff -r dd9cfc512b7f -r c7ce7685e087 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Jul 21 15:23:46 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Jul 21 15:31:38 2010 +0200
@@ -16,7 +16,6 @@
   val if_known_thy: (string -> unit) -> string -> unit
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
-  val the_theory: string -> theory -> theory
   val is_finished: string -> bool
   val master_directory: string -> Path.T
   val loaded_files: string -> Path.T list
@@ -176,10 +175,6 @@
     SOME theory => theory
   | _ => error (loader_msg "undefined theory entry for" [name]));
 
-fun the_theory name thy =
-  if Context.theory_name thy = name then thy
-  else get_theory name;
-
 
 
 (** thy operations **)
diff -r dd9cfc512b7f -r c7ce7685e087 src/Pure/context.ML
--- a/src/Pure/context.ML	Wed Jul 21 15:23:46 2010 +0200
+++ b/src/Pure/context.ML	Wed Jul 21 15:31:38 2010 +0200
@@ -41,6 +41,7 @@
   val pretty_abbrev_thy: theory -> Pretty.T
   val str_of_thy: theory -> string
   val get_theory: theory -> string -> theory
+  val this_theory: theory -> string -> theory
   val deref: theory_ref -> theory
   val check_thy: theory -> theory_ref
   val eq_thy: theory * theory -> bool
@@ -253,6 +254,10 @@
   else if #stage (history_of thy) = finished then thy
   else error ("Unfinished theory " ^ quote name);
 
+fun this_theory thy name =
+  if theory_name thy = name then thy
+  else get_theory thy name;
+
 
 (* theory references *)
 
diff -r dd9cfc512b7f -r c7ce7685e087 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Jul 21 15:23:46 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Wed Jul 21 15:31:38 2010 +0200
@@ -910,7 +910,7 @@
     fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
     fun read_const_expr "*" = ([], consts_of thy)
       | read_const_expr s = if String.isSuffix ".*" s
-          then ([], consts_of_select (Thy_Info.the_theory (unsuffix ".*" s) thy))
+          then ([], consts_of_select (Context.this_theory thy (unsuffix ".*" s)))
           else ([Code.read_const thy s], []);
   in pairself flat o split_list o map read_const_expr end;