# HG changeset patch
# User wenzelm
# Date 1217935891 -7200
# Node ID 66596d7aa899dc27e4f61f99c24ceecd9ff1f75a
# Parent  302e9c8c489b9b25480f6dc8987d78d4f083a3be
Facts.lookup: return static/dynamic status;

diff -r 302e9c8c489b -r 66596d7aa899 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Aug 04 22:55:10 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Aug 05 13:31:31 2008 +0200
@@ -859,7 +859,7 @@
           if name = "" then [Thm.transfer thy Drule.dummy_thm]
           else
             (case Facts.lookup (Context.Proof ctxt) local_facts name of
-              SOME ths => map (Thm.transfer thy) (Facts.select thmref ths)
+              SOME (_, ths) => map (Thm.transfer thy) (Facts.select thmref ths)
             | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref);
       in pick name thms end;
 
diff -r 302e9c8c489b -r 66596d7aa899 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Mon Aug 04 22:55:10 2008 +0200
+++ b/src/Pure/facts.ML	Tue Aug 05 13:31:31 2008 +0200
@@ -23,7 +23,7 @@
   val empty: T
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
-  val lookup: Context.generic -> T -> string -> thm list option
+  val lookup: Context.generic -> T -> string -> (bool * thm list) option
   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
@@ -144,8 +144,8 @@
 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));
+  | SOME (Static ths, _) => SOME (true, ths)
+  | SOME (Dynamic f, _) => SOME (false, f context));
 
 fun fold_static f = Symtab.fold (fn (name, (Static ths, _)) => f (name, ths) | _ => I) o table_of;