# HG changeset patch
# User wenzelm
# Date 1465326788 -7200
# Node ID 3f594efa9504d053333efe2eeca52c3b873a9700
# Parent  7bd64a07fe43ecbb09a2b04e769341ab8c174262
clarified signature;

diff -r 7bd64a07fe43 -r 3f594efa9504 src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Tue Jun 07 20:45:07 2016 +0200
+++ b/src/HOL/Eisbach/method_closure.ML	Tue Jun 07 21:13:08 2016 +0200
@@ -122,7 +122,7 @@
       text |> (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
+                SOME {dynamic = true, thms} => K thms
               | _ => I)
           | NONE => I);
     val ctxt' = Config.put Method.closure false ctxt;
diff -r 7bd64a07fe43 -r 3f594efa9504 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jun 07 20:45:07 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Jun 07 21:13:08 2016 +0200
@@ -116,7 +116,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 lookup_fact: Proof.context -> string -> {dynamic: bool, thms: 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
@@ -1008,23 +1008,23 @@
   | retrieve pick context (Facts.Named ((xname, pos), sel)) =
       let
         val thy = Context.theory_of context;
-        fun immediate thm = {name = xname, static = true, thms = [Thm.transfer thy thm]};
-        val {name, static, thms} =
+        fun immediate thm = {name = xname, dynamic = false, thms = [Thm.transfer thy thm]};
+        val {name, dynamic, thms} =
           (case xname of
             "" => immediate Drule.dummy_thm
           | "_" => immediate Drule.asm_rl
           | _ => retrieve_generic context (xname, pos));
         val thms' =
-          if not static andalso Config.get_generic context dynamic_facts_dummy
+          if dynamic 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 pick (dynamic andalso is_none sel) (name, pos) thms' end;
 
 in
 
 val get_fact_generic =
-  retrieve (fn static => fn (name, _) => fn thms =>
-    (if static then NONE else SOME name, thms));
+  retrieve (fn dynamic => fn (name, _) => fn thms =>
+    (if dynamic then SOME name else NONE, thms));
 
 val get_fact = retrieve (K (K I)) o Context.Proof;
 val get_fact_single = retrieve (K Facts.the_single) o Context.Proof;
diff -r 7bd64a07fe43 -r 3f594efa9504 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Tue Jun 07 20:45:07 2016 +0200
+++ b/src/Pure/facts.ML	Tue Jun 07 21:13:08 2016 +0200
@@ -30,9 +30,9 @@
   val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
   val defined: T -> string -> bool
   val is_dynamic: T -> string -> bool
-  val lookup: Context.generic -> T -> string -> (bool * thm list) option
+  val lookup: Context.generic -> T -> string -> {dynamic: bool, thms: thm list} option
   val retrieve: Context.generic -> T -> xstring * Position.T ->
-    {name: string, static: bool, thms: thm list}
+    {name: string, dynamic: bool, thms: thm list}
   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
   val dest_static: bool -> T list -> T -> (string * thm list) list
   val dest_all: Context.generic -> bool -> T list -> T -> (string * thm list) list
@@ -178,22 +178,23 @@
 fun lookup context facts name =
   (case Name_Space.lookup (facts_of facts) name of
     NONE => NONE
-  | SOME (Static ths) => SOME (true, ths)
-  | SOME (Dynamic f) => SOME (false, f context));
+  | SOME (Static ths) => SOME {dynamic = false, thms = ths}
+  | SOME (Dynamic f) => SOME {dynamic = true, thms = f context});
 
 fun retrieve context facts (xname, pos) =
   let
     val name = check context facts (xname, pos);
-    val (static, thms) =
+    val {dynamic, thms} =
       (case lookup context facts name of
-        SOME (static, thms) =>
-          (if static then ()
-           else Context_Position.report_generic context pos (Markup.dynamic_fact name);
-           (static, thms))
+        SOME res =>
+          (if #dynamic res
+           then Context_Position.report_generic context pos (Markup.dynamic_fact name)
+           else ();
+           res)
       | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
   in
    {name = name,
-    static = static,
+    dynamic = dynamic,
     thms = map (Thm.transfer (Context.theory_of context)) thms}
   end;