# HG changeset patch
# User wenzelm
# Date 1205873855 -3600
# Node ID 5fe18f9493eff6ef85f923e8e40e7c5ca6e09666
# Parent  f512d78e66875fa174854768460b6f59650fb8af
removed check_lookup;
added get_thms_silent;

diff -r f512d78e6687 -r 5fe18f9493ef src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Mar 18 21:27:25 2008 +0100
+++ b/src/Pure/pure_thy.ML	Tue Mar 18 21:57:35 2008 +0100
@@ -50,7 +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 get_thms_silent: theory -> thmref -> thm list
   val theorems_of: theory -> thm list NameSpace.table
   val all_facts_of: theory -> Facts.T
   val thms_of: theory -> (string * thm) list
@@ -251,8 +251,6 @@
 
 (* lookup/get thms *)
 
-val check_lookup = ref false;
-
 local
 
 fun lookup_thms thy xname =
@@ -270,9 +268,7 @@
 fun show_result NONE = "none"
   | show_result (SOME (name, _)) = quote name;
 
-in
-
-fun get_thms theory thmref =
+fun get_fact silent theory thmref =
   let
     val name = name_of_thmref thmref;
     val new_res = lookup_fact theory name;
@@ -283,12 +279,16 @@
       | (SOME (name1, ths1), SOME (name2, ths2)) => name1 = name2 andalso Thm.eq_thms (ths1, ths2)
       | _ => false);
     val _ =
-      if is_same orelse not (! check_lookup) then ()
+      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 |> select_thm thmref |> map (Thm.transfer theory) end;
 
+in
+
+val get_thms_silent = get_fact true;
+val get_thms = get_fact false;
 fun get_thmss thy thmrefs = maps (get_thms thy) thmrefs;
 fun get_thm thy thmref = single_thm (name_of_thmref thmref) (get_thms thy thmref);