Facts.lookup: return static/dynamic status;
authorwenzelm
Tue Aug 05 13:31:31 2008 +0200 (2008-08-05 ago)
changeset 2773866596d7aa899
parent 27737 302e9c8c489b
child 27739 cd1df29db620
Facts.lookup: return static/dynamic status;
src/Pure/Isar/proof_context.ML
src/Pure/facts.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Aug 04 22:55:10 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Aug 05 13:31:31 2008 +0200
     1.3 @@ -859,7 +859,7 @@
     1.4            if name = "" then [Thm.transfer thy Drule.dummy_thm]
     1.5            else
     1.6              (case Facts.lookup (Context.Proof ctxt) local_facts name of
     1.7 -              SOME ths => map (Thm.transfer thy) (Facts.select thmref ths)
     1.8 +              SOME (_, ths) => map (Thm.transfer thy) (Facts.select thmref ths)
     1.9              | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref);
    1.10        in pick name thms end;
    1.11  
     2.1 --- a/src/Pure/facts.ML	Mon Aug 04 22:55:10 2008 +0200
     2.2 +++ b/src/Pure/facts.ML	Tue Aug 05 13:31:31 2008 +0200
     2.3 @@ -23,7 +23,7 @@
     2.4    val empty: T
     2.5    val intern: T -> xstring -> string
     2.6    val extern: T -> string -> xstring
     2.7 -  val lookup: Context.generic -> T -> string -> thm list option
     2.8 +  val lookup: Context.generic -> T -> string -> (bool * thm list) option
     2.9    val defined: T -> string -> bool
    2.10    val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
    2.11    val dest_static: T list -> T -> (string * thm list) list
    2.12 @@ -144,8 +144,8 @@
    2.13  fun lookup context facts name =
    2.14    (case Symtab.lookup (table_of facts) name of
    2.15      NONE => NONE
    2.16 -  | SOME (Static ths, _) => SOME ths
    2.17 -  | SOME (Dynamic f, _) => SOME (f context));
    2.18 +  | SOME (Static ths, _) => SOME (true, ths)
    2.19 +  | SOME (Dynamic f, _) => SOME (false, f context));
    2.20  
    2.21  fun fold_static f = Symtab.fold (fn (name, (Static ths, _)) => f (name, ths) | _ => I) o table_of;
    2.22