src/Pure/pure_thy.ML

   val single_thm: string -> thm list -> thm
   val name_of_thmref: thmref -> string
   val map_name_of_thmref: (string -> string) -> thmref -> thmref
   val select_thm: thmref -> thm list -> thm list
   val selections: string * thm list -> (thmref * thm) list
+  val check_lookup: bool ref
   val theorems_of: theory -> thm list NameSpace.table
   val all_facts_of: theory -> Facts.T
   val thms_of: theory -> (string * thm) list
   val all_thms_of: theory -> (string * thm) list
   val hide_thms: bool -> string list -> theory -> theory

       (NameSelection (name, [Single i]), thm));
 
 
 (* lookup/get thms *)
 
+val check_lookup = ref false;
+
 local
 
 fun lookup_thms thy xname =
   let
     val (space, thms) = #theorems (get_theorems thy);

       (case (new_res, old_res) of
         (NONE, NONE) => true
       | (SOME (name1, ths1), SOME (name2, ths2)) => name1 = name2 andalso Thm.eq_thms (ths1, ths2)
       | _ => false);
     val _ =
-      if is_same then ()
+      if is_same orelse not (! check_lookup) 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 |> select_thm thmref |> map (Thm.transfer theory) end;