# HG changeset patch
# User wenzelm
# Date 935073216 -7200
# Node ID 21ff5bb68a5cd20afbbb849da9ab24caf92ade25
# Parent  d603a06b30df9f456b36fcb0853767f87bb4f316
lookup_theory;

diff -r d603a06b30df -r 21ff5bb68a5c src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Aug 19 15:22:12 1999 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Aug 19 16:33:36 1999 +0200
@@ -28,6 +28,7 @@
   val str_of_action: action -> string
   val add_hook: (action -> string -> unit) -> unit
   val names: unit -> string list
+  val lookup_theory: string -> theory option
   val get_theory: string -> theory
   val get_preds: string -> string list
   val loaded_files: string -> ((Path.T * File.info) * bool) list
@@ -151,9 +152,11 @@
 
 (* access theory *)
 
+fun lookup_theory name = #2 (get_thy name);
+
 fun get_theory name =
-  (case get_thy name of
-    (_, Some theory) => theory
+  (case lookup_theory name of
+    (Some theory) => theory
   | _ => error (loader_msg "undefined theory entry for" [name]));
 
 val theory_of_sign = get_theory o Sign.name_of;
@@ -194,7 +197,7 @@
 
 fun check_unfinished fail name =
   if is_some (lookup_thy name) andalso is_finished name then
-    fail (loader_msg "cannot change finished theory" [name])
+    fail (loader_msg "cannot update finished theory" [name])
   else ();