# HG changeset patch
# User wenzelm
# Date 1208360439 -7200
# Node ID 8492816588594a4730c8dcd5e6f733c11966b28d
# Parent  310c3b1a4157e65e577f97606544c8d8770a67dc
removed obsolete get_fact_silent;
PureThy.get_fact: pass dynamic context;
tuned;

diff -r 310c3b1a4157 -r 849281658859 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Apr 16 17:40:38 2008 +0200
+++ b/src/Pure/pure_thy.ML	Wed Apr 16 17:40:39 2008 +0200
@@ -26,8 +26,7 @@
   val is_internal: thm -> bool
   val intern_fact: theory -> xstring -> string
   val check_fact: theory -> string -> bool
-  val get_fact: theory -> Facts.ref -> thm list
-  val get_fact_silent: theory -> Facts.ref -> thm list
+  val get_fact: Context.generic -> theory -> Facts.ref -> thm list
   val get_thms: theory -> xstring -> thm list
   val get_thm: theory -> xstring -> thm
   val theorems_of: theory -> thm list NameSpace.table
@@ -164,37 +163,31 @@
     val name = NameSpace.intern space xname;
   in Option.map (pair name) (Symtab.lookup thms name) end;
 
-fun lookup_fact thy xname =
+fun lookup_fact context thy xname =
   let val name = intern_fact thy xname
-  in Option.map (pair name) (Facts.lookup (Context.Theory thy) (facts_of thy) name) end;
-
-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 _ = Theory.check_thy theory;
-    val is_same =
-      (case (new_res, old_res) of
-        (SOME (_, ths1), SOME (_, ths2)) => Thm.eq_thms (ths1, ths2)
-      | _ => true);
-    val _ =
-      if is_same orelse silent then ()
-      else error ("Fact lookup differs from old-style thm database:\n" ^
-        fst (the new_res) ^ " vs " ^ fst (the old_res) ^ Position.str_of pos);
-  in
-    (case new_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 Option.map (pair name) (Facts.lookup context (facts_of thy) name) end;
 
 in
 
-val get_fact_silent = get true;
-val get_fact = get false;
+fun get_fact context theory xthmref =
+  let
+    val xname = Facts.name_of_ref xthmref;
+    val pos = Facts.pos_of_ref xthmref;
+    val new_res = lookup_fact context theory xname;
+    val old_res = get_first (fn thy => lookup_thms thy xname) (theory :: Theory.ancestors_of theory);
+    val _ = Theory.check_thy theory;
+  in
+    (case (new_res, old_res) of
+      (SOME (_, ths1), SOME (_, ths2)) => Thm.eq_thms (ths1, ths2) orelse
+        error ("Fact lookup differs from old-style thm database:\n" ^
+          fst (the new_res) ^ " vs " ^ fst (the old_res) ^ Position.str_of pos)
+    | _ => true);
+    (case new_res of
+      NONE => error ("Unknown fact " ^ quote xname ^ Position.str_of pos)
+    | SOME (_, ths) => Facts.select xthmref (map (Thm.transfer theory) ths))
+  end;
 
-fun get_thms thy = get_fact thy o Facts.named;
+fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named;
 fun get_thm thy name = Facts.the_single name (get_thms thy name);
 
 end;
@@ -310,7 +303,7 @@
 
 in
 
-fun note_thmss k = gen_note_thmss get_fact (kind k);
+fun note_thmss k = gen_note_thmss (fn thy => get_fact (Context.Theory thy) thy) (kind k);
 fun note_thmss_i k = gen_note_thmss (K I) (kind k);
 fun note_thmss_grouped k g = gen_note_thmss (K I) (kind k #> group g);