src/Pure/facts.ML
changeset 59883 12a89103cae6
parent 59058 a78612c67ec0
child 59884 bbf49d7dfd6f
equal deleted inserted replaced
59882:ada832308efe 59883:12a89103cae6
   164 fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of;
   164 fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of;
   165 
   165 
   166 
   166 
   167 (* retrieve *)
   167 (* retrieve *)
   168 
   168 
   169 val defined = is_some oo (Name_Space.lookup_key o facts_of);
   169 val defined = Name_Space.defined o facts_of;
   170 
   170 
   171 fun lookup context facts name =
   171 fun lookup context facts name =
   172   (case Name_Space.lookup_key (facts_of facts) name of
   172   (case Name_Space.lookup_key (facts_of facts) name of
   173     NONE => NONE
   173     NONE => NONE
   174   | SOME (_, Static ths) => SOME (true, ths)
   174   | SOME (_, Static ths) => SOME (true, ths)