1.1 --- a/src/Pure/facts.ML	Tue Apr 15 18:49:16 2008 +0200
     1.2 +++ b/src/Pure/facts.ML	Tue Apr 15 18:49:18 2008 +0200
     1.3 @@ -22,9 +22,11 @@
     1.4    type T
     1.5    val empty: T
     1.6    val space_of: T -> NameSpace.T
     1.7 +  val intern: T -> xstring -> string
     1.8 +  val extern: T -> string -> xstring
     1.9    val lookup: Context.generic -> T -> string -> thm list option
    1.10 -  val dest: T -> (string * thm list) list
    1.11 -  val extern: T -> (xstring * thm list) list
    1.12 +  val dest_table: T -> (string * thm list) list
    1.13 +  val extern_table: T -> (xstring * thm list) list
    1.14    val props: T -> thm list
    1.15    val could_unify: T -> term -> thm list
    1.16    val merge: T * T -> T
    1.17 @@ -133,18 +135,21 @@
    1.18  val space_of = #1 o facts_of;
    1.19  val table_of = #2 o facts_of;
    1.20  
    1.21 +val intern = NameSpace.intern o space_of;
    1.22 +val extern = NameSpace.extern o space_of;
    1.23 +
    1.24  fun lookup context facts name =
    1.25    (case Symtab.lookup (table_of facts) name of
    1.26      NONE => NONE
    1.27    | SOME (Static ths, _) => SOME ths
    1.28    | SOME (Dynamic f, _) => SOME (f context));
    1.29  
    1.30 -fun dest facts =
    1.31 +fun dest_table facts =
    1.32    Symtab.fold (fn (name, (Static ths, _)) => cons (name, ths) | _ => I) (table_of facts) [];
    1.33  
    1.34 -fun extern facts =
    1.35 -  dest facts
    1.36 -  |> map (apfst (NameSpace.extern (space_of facts)))
    1.37 +fun extern_table facts =
    1.38 +  dest_table facts
    1.39 +  |> map (apfst (extern facts))
    1.40    |> sort_wrt #1;
    1.41  
    1.42