# HG changeset patch
# User wenzelm
# Date 1206031134 -3600
# Node ID 06635166d211c3ab3729de5c737dbec4e058ff08
# Parent  5c089f4219c2044caf6e68c568b2229975af4b0c
get_thms etc.: improved reporting of source position;

diff -r 5c089f4219c2 -r 06635166d211 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Mar 20 17:38:53 2008 +0100
+++ b/src/Pure/pure_thy.ML	Thu Mar 20 17:38:54 2008 +0100
@@ -168,9 +168,6 @@
 
 (** retrieve theorems **)
 
-fun the_thms _ (SOME thms) = thms
-  | the_thms name NONE = error ("Unknown theorem(s) " ^ quote name);
-
 local
 
 fun lookup_thms thy xname =
@@ -191,6 +188,7 @@
 fun get silent theory thmref =
   let
     val name = Facts.name_of_ref thmref;
+    val pos = Facts.pos_of_ref thmref;
     val new_res = lookup_fact theory name;
     val old_res = get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory);
     val is_same =
@@ -201,9 +199,12 @@
     val _ =
       if is_same orelse silent then ()
       else legacy_feature ("Fact lookup differs from old-style thm database:\n" ^
-        show_result new_res ^ " vs " ^ show_result old_res ^
-        Position.str_of (Position.thread_data ()));
-  in Option.map #2 old_res |> the_thms name |> Facts.select thmref |> map (Thm.transfer theory) end;
+        show_result new_res ^ " vs " ^ show_result old_res ^ Position.str_of pos);
+  in
+    (case old_res of
+      NONE => error ("Unknown theorem(s) " ^ quote name ^ Position.str_of pos)
+    | SOME (_, ths) => Facts.select thmref (map (Thm.transfer theory) ths))
+  end;
 
 in