src/Pure/facts.ML
changeset 27738 66596d7aa899
parent 27175 620295a57106
child 28864 d6fe93e3dcb9
     1.1 --- a/src/Pure/facts.ML	Mon Aug 04 22:55:10 2008 +0200
     1.2 +++ b/src/Pure/facts.ML	Tue Aug 05 13:31:31 2008 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4    val empty: T
     1.5    val intern: T -> xstring -> string
     1.6    val extern: T -> string -> xstring
     1.7 -  val lookup: Context.generic -> T -> string -> thm list option
     1.8 +  val lookup: Context.generic -> T -> string -> (bool * thm list) option
     1.9    val defined: T -> string -> bool
    1.10    val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
    1.11    val dest_static: T list -> T -> (string * thm list) list
    1.12 @@ -144,8 +144,8 @@
    1.13  fun lookup context facts name =
    1.14    (case Symtab.lookup (table_of facts) name of
    1.15      NONE => NONE
    1.16 -  | SOME (Static ths, _) => SOME ths
    1.17 -  | SOME (Dynamic f, _) => SOME (f context));
    1.18 +  | SOME (Static ths, _) => SOME (true, ths)
    1.19 +  | SOME (Dynamic f, _) => SOME (false, f context));
    1.20  
    1.21  fun fold_static f = Symtab.fold (fn (name, (Static ths, _)) => f (name, ths) | _ => I) o table_of;
    1.22