src/Pure/facts.ML

--- a/src/Pure/facts.ML	Tue Apr 15 18:49:16 2008 +0200
+++ b/src/Pure/facts.ML	Tue Apr 15 18:49:18 2008 +0200
@@ -22,9 +22,11 @@
   type T
   val empty: T
   val space_of: T -> NameSpace.T
+  val intern: T -> xstring -> string
+  val extern: T -> string -> xstring
   val lookup: Context.generic -> T -> string -> thm list option
-  val dest: T -> (string * thm list) list
-  val extern: T -> (xstring * thm list) list
+  val dest_table: T -> (string * thm list) list
+  val extern_table: T -> (xstring * thm list) list
   val props: T -> thm list
   val could_unify: T -> term -> thm list
   val merge: T * T -> T
@@ -133,18 +135,21 @@
 val space_of = #1 o facts_of;
 val table_of = #2 o facts_of;
 
+val intern = NameSpace.intern o space_of;
+val extern = NameSpace.extern o space_of;
+
 fun lookup context facts name =
   (case Symtab.lookup (table_of facts) name of
     NONE => NONE
   | SOME (Static ths, _) => SOME ths
   | SOME (Dynamic f, _) => SOME (f context));
 
-fun dest facts =
+fun dest_table facts =
   Symtab.fold (fn (name, (Static ths, _)) => cons (name, ths) | _ => I) (table_of facts) [];
 
-fun extern facts =
-  dest facts
-  |> map (apfst (NameSpace.extern (space_of facts)))
+fun extern_table facts =
+  dest_table facts
+  |> map (apfst (extern facts))
   |> sort_wrt #1;