# HG changeset patch
# User wenzelm
# Date 1205872045 -3600
# Node ID f512d78e66875fa174854768460b6f59650fb8af
# Parent  967323f93c675cd302d8755943e5a94753842122
added ckeck_lookup flag (default false), which controls sanity check of thm lookup;

diff -r 967323f93c67 -r f512d78e6687 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Mar 18 20:34:26 2008 +0100
+++ b/src/Pure/pure_thy.ML	Tue Mar 18 21:27:25 2008 +0100
@@ -50,6 +50,7 @@
   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
@@ -250,6 +251,8 @@
 
 (* lookup/get thms *)
 
+val check_lookup = ref false;
+
 local
 
 fun lookup_thms thy xname =
@@ -280,7 +283,7 @@
       | (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 ()));