--- a/src/Pure/Isar/proof_context.ML Wed Jan 06 10:20:33 2016 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Jan 06 11:45:07 2016 +0100
@@ -119,6 +119,7 @@
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 dynamic_facts_dummy: bool Config.T
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
@@ -941,7 +942,7 @@
end;
-(* get facts *)
+(* lookup facts *)
fun lookup_fact ctxt name =
let
@@ -953,6 +954,12 @@
| some => some)
end;
+
+(* retrieve facts *)
+
+val dynamic_facts_dummy =
+ Config.bool (Config.declare ("dynamic_facts_dummy_", @{here}) (fn _ => Config.Bool false));
+
local
fun retrieve_global context =
@@ -991,7 +998,10 @@
"" => immediate Drule.dummy_thm
| "_" => immediate Drule.asm_rl
| _ => retrieve_generic context (xname, pos));
- val thms' = Facts.select (Facts.Named ((name, pos), sel)) thms;
+ val thms' =
+ if not static andalso Config.get_generic context dynamic_facts_dummy
+ then [Drule.free_dummy_thm]
+ else Facts.select (Facts.Named ((name, pos), sel)) thms;
in pick (static orelse is_some sel) (name, pos) thms' end;
in