# HG changeset patch
# User wenzelm
# Date 1452077107 -3600
# Node ID 76399b8fde4d7bf64f0cc36087512ba16acde139
# Parent  e8ae72c2602555f57a94a5ac452dfd5f9e06c0ff
more systematic treatment of dynamic facts, when forming closure;

diff -r e8ae72c26025 -r 76399b8fde4d src/HOL/Eisbach/Tests.thy
--- a/src/HOL/Eisbach/Tests.thy	Wed Jan 06 10:20:33 2016 +0100
+++ b/src/HOL/Eisbach/Tests.thy	Wed Jan 06 11:45:07 2016 +0100
@@ -497,6 +497,19 @@
 lemma "A \<Longrightarrow> A" by test2
 
 
+subsection \<open>Dynamic facts\<close>
+
+named_theorems my_thms_named'
+
+method foo_method1 for x =
+  (match my_thms_named' [of (unchecked) x] in R: "PROP ?H" \<Rightarrow> \<open>rule R\<close>)
+
+lemma
+  assumes A [my_thms_named']: "\<And>x. A x"
+  shows "A y"
+  by (foo_method1 y)
+
+
 subsection \<open>Eisbach method invocation from ML\<close>
 
 method test_method for x y uses r = (print_term x, print_term y, rule r)
diff -r e8ae72c26025 -r 76399b8fde4d src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Wed Jan 06 10:20:33 2016 +0100
+++ b/src/HOL/Eisbach/method_closure.ML	Wed Jan 06 11:45:07 2016 +0100
@@ -251,11 +251,11 @@
          Method.sections modifiers)) >> (fn (ts, decl) => meth ts o decl);
 
     val lthy3 = lthy2
-      |> fold dummy_named_thm named_thms
       |> Method.local_setup (Binding.make (Binding.name_of name, Position.none))
         (parser term_args get_recursive_method) "(internal)";
 
-    val (text, src) = read_closure lthy3 source;
+    val (text, src) =
+      read_closure (Config.put Proof_Context.dynamic_facts_dummy true lthy3) source;
 
     val morphism =
       Variable.export_morphism lthy3
diff -r e8ae72c26025 -r 76399b8fde4d src/Pure/Isar/proof_context.ML
--- 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