src/Pure/facts.ML

   val check: Context.generic -> T -> xstring * Position.T -> string
   val intern: T -> xstring -> string
   val extern: Proof.context -> T -> string -> xstring
   val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
   val lookup: Context.generic -> T -> string -> (bool * thm list) option
-  val retrieve: Context.generic -> T -> xstring * Position.T -> string * thm list
+  val retrieve: Context.generic -> T -> xstring * Position.T ->
+    {name: string, static: bool, thms: thm list}
   val defined: T -> string -> bool
   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
   val dest_static: bool -> T list -> T -> (string * thm list) list
   val props: T -> thm list
   val could_unify: T -> term -> thm list

   | SOME (_, Dynamic f) => SOME (false, f context));
 
 fun retrieve context facts (xname, pos) =
   let
     val name = check context facts (xname, pos);
-    val thms =
+    val (static, thms) =
       (case lookup context facts name of
         SOME (static, thms) =>
           (if static then ()
            else Context_Position.report_generic context pos (Markup.dynamic_fact name);
-           thms)
+           (static, thms))
       | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
-  in (name, map (Thm.transfer (Context.theory_of context)) thms) end;
+  in
+   {name = name,
+    static = static,
+    thms = map (Thm.transfer (Context.theory_of context)) thms}
+  end;
 
 
 (* static content *)
 
 fun fold_static f =