1.1 --- a/src/Pure/pure_thy.ML	Thu Mar 20 17:38:53 2008 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Thu Mar 20 17:38:54 2008 +0100
     1.3 @@ -168,9 +168,6 @@
     1.4  
     1.5  (** retrieve theorems **)
     1.6  
     1.7 -fun the_thms _ (SOME thms) = thms
     1.8 -  | the_thms name NONE = error ("Unknown theorem(s) " ^ quote name);
     1.9 -
    1.10  local
    1.11  
    1.12  fun lookup_thms thy xname =
    1.13 @@ -191,6 +188,7 @@
    1.14  fun get silent theory thmref =
    1.15    let
    1.16      val name = Facts.name_of_ref thmref;
    1.17 +    val pos = Facts.pos_of_ref thmref;
    1.18      val new_res = lookup_fact theory name;
    1.19      val old_res = get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory);
    1.20      val is_same =
    1.21 @@ -201,9 +199,12 @@
    1.22      val _ =
    1.23        if is_same orelse silent then ()
    1.24        else legacy_feature ("Fact lookup differs from old-style thm database:\n" ^
    1.25 -        show_result new_res ^ " vs " ^ show_result old_res ^
    1.26 -        Position.str_of (Position.thread_data ()));
    1.27 -  in Option.map #2 old_res |> the_thms name |> Facts.select thmref |> map (Thm.transfer theory) end;
    1.28 +        show_result new_res ^ " vs " ^ show_result old_res ^ Position.str_of pos);
    1.29 +  in
    1.30 +    (case old_res of
    1.31 +      NONE => error ("Unknown theorem(s) " ^ quote name ^ Position.str_of pos)
    1.32 +    | SOME (_, ths) => Facts.select thmref (map (Thm.transfer theory) ths))
    1.33 +  end;
    1.34  
    1.35  in
    1.36