--- 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
--- 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 =