# HG changeset patch
# User wenzelm
# Date 1450790417 -3600
# Node ID 4d162c237e4819f2c5fc41650354e8334c94dee7
# Parent  653337546fad1152fa2bfb8431eef77ea3c6474e
more accurate lookup of dynamic facts;

diff -r 653337546fad -r 4d162c237e48 src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Tue Dec 22 11:25:21 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML	Tue Dec 22 14:20:17 2015 +0100
@@ -147,20 +147,17 @@
   in (named_thm, parser) end;
 
 
-fun evaluate_dynamic_thm ctxt name =
-  (case try (Named_Theorems.get ctxt) name of
-    SOME thms => thms
-  | NONE => Proof_Context.get_thms ctxt name);
-
-
-fun evaluate_named_theorems ctxt =
-  (Method.map_source o map o Token.map_facts)
-    (fn SOME name => K (evaluate_dynamic_thm ctxt name) | NONE => I);
-
 fun method_evaluate text ctxt facts =
-  let val ctxt' = Config.put Method.closure false ctxt in
-    Method.RUNTIME (fn st => Method.evaluate (evaluate_named_theorems ctxt' text) ctxt' facts st)
-  end;
+  let
+    val eval_named_theorems =
+      (Method.map_source o map o Token.map_facts)
+        (fn SOME name =>
+              (case Proof_Context.lookup_fact ctxt name of
+                SOME (false, ths) => K ths
+              | _ => I)
+          | NONE => I);
+    val ctxt' = Config.put Method.closure false ctxt;
+  in Method.RUNTIME (fn st => Method.evaluate (eval_named_theorems text) ctxt' facts st) end;
 
 fun method_instantiate env text =
   let
diff -r 653337546fad -r 4d162c237e48 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Dec 22 11:25:21 2015 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Dec 22 14:20:17 2015 +0100
@@ -118,6 +118,7 @@
     (term list list * (indexname * term) list)
   val fact_tac: Proof.context -> thm list -> int -> tactic
   val some_fact_tac: Proof.context -> int -> tactic
+  val lookup_fact: Proof.context -> string -> (bool * thm list) option
   val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list
   val get_fact: Proof.context -> Facts.ref -> thm list
   val get_fact_single: Proof.context -> Facts.ref -> thm
@@ -942,6 +943,16 @@
 
 (* get facts *)
 
+fun lookup_fact ctxt name =
+  let
+    val context = Context.Proof ctxt;
+    val thy = Proof_Context.theory_of ctxt;
+  in
+    (case Facts.lookup context (facts_of ctxt) name of
+      NONE => Facts.lookup context (Global_Theory.facts_of thy) name
+    | some => some)
+  end;
+
 local
 
 fun retrieve_global context =