src/Pure/facts.ML

--- a/src/Pure/facts.ML	Thu Mar 13 17:26:22 2014 +0100
+++ b/src/Pure/facts.ML	Fri Mar 14 10:08:36 2014 +0100
@@ -26,7 +26,9 @@
   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 defined: T -> string -> bool
   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
   val dest_static: T list -> T -> (string * thm list) list
@@ -155,6 +157,7 @@
 
 val intern = Name_Space.intern o space_of;
 fun extern ctxt = Name_Space.extern ctxt o space_of;
+fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of
 
 val defined = is_some oo (Name_Space.lookup_key o facts_of);
 
@@ -164,6 +167,18 @@
   | SOME (_, Static ths) => SOME (true, ths)
   | SOME (_, Dynamic f) => SOME (false, f context));
 
+fun retrieve context facts (xname, pos) =
+  let
+    val name = check context facts (xname, pos);
+    val 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)
+      | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
+  in (name, map (Thm.transfer (Context.theory_of context)) thms) end;
+
 fun fold_static f =
   Name_Space.fold_table (fn (name, Static ths) => f (name, ths) | _ => I) o facts_of;