src/Pure/facts.ML

--- a/src/Pure/facts.ML	Thu Aug 14 14:28:11 2014 +0200
+++ b/src/Pure/facts.ML	Thu Aug 14 16:20:14 2014 +0200
@@ -29,7 +29,8 @@
   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
@@ -176,14 +177,18 @@
 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 *)