src/Pure/facts.ML
changeset 26692 3f48d4f4229f
parent 26664 167d879a89b0
child 27175 620295a57106
     1.1 --- a/src/Pure/facts.ML	Wed Apr 16 21:52:59 2008 +0200
     1.2 +++ b/src/Pure/facts.ML	Wed Apr 16 21:53:00 2008 +0200
     1.3 @@ -21,12 +21,13 @@
     1.4    val selections: string * thm list -> (ref * thm) list
     1.5    type T
     1.6    val empty: T
     1.7 -  val space_of: T -> NameSpace.T
     1.8    val intern: T -> xstring -> string
     1.9    val extern: T -> string -> xstring
    1.10    val lookup: Context.generic -> T -> string -> thm list option
    1.11 -  val dest_table: T -> (string * thm list) list
    1.12 -  val extern_table: T -> (xstring * thm list) list
    1.13 +  val defined: T -> string -> bool
    1.14 +  val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
    1.15 +  val dest_static: T -> (string * thm list) list
    1.16 +  val extern_static: T -> (xstring * thm list) list
    1.17    val props: T -> thm list
    1.18    val could_unify: T -> term -> thm list
    1.19    val merge: T * T -> T
    1.20 @@ -138,19 +139,19 @@
    1.21  val intern = NameSpace.intern o space_of;
    1.22  val extern = NameSpace.extern o space_of;
    1.23  
    1.24 +val defined = Symtab.defined o table_of;
    1.25 +
    1.26  fun lookup context facts name =
    1.27    (case Symtab.lookup (table_of facts) name of
    1.28      NONE => NONE
    1.29    | SOME (Static ths, _) => SOME ths
    1.30    | SOME (Dynamic f, _) => SOME (f context));
    1.31  
    1.32 -fun dest_table facts =
    1.33 -  Symtab.fold (fn (name, (Static ths, _)) => cons (name, ths) | _ => I) (table_of facts) [];
    1.34 +fun fold_static f = Symtab.fold (fn (name, (Static ths, _)) => f (name, ths) | _ => I) o table_of;
    1.35  
    1.36 -fun extern_table facts =
    1.37 -  dest_table facts
    1.38 -  |> map (apfst (extern facts))
    1.39 -  |> sort_wrt #1;
    1.40 +fun dest_static facts = sort_wrt #1 (fold_static cons facts []);
    1.41 +fun extern_static facts =
    1.42 +  sort_wrt #1 (fold_static (fn (name, ths) => cons (extern facts name, ths)) facts []);
    1.43  
    1.44  
    1.45  (* indexed props *)