Nicer names in FindTheorems. * Patch NameSpace.get_accesses, contributed by Timothy Bourke: NameSpace.get_accesses has been patched to fix the following bug: theory OverHOL imports Main begin lemma conjI: "a & b --> b" by blast ML {* val ns = PureThy.facts_of @{theory} |> Facts.space_of; val x1 = NameSpace.get_accesses ns "HOL.conjI"; val x2 = NameSpace.get_accesses ns "OverHOL.conjI"; *} end where x1 = ["conjI", "HOL.conjI"] and x2 = ["conjI", "OverHOL.conjI"], but x1 should be just ["HOL.conjI"]. NameSpace.get_accesses is only used within the NameSpace structure itself. The two uses have been modified to retain their original behaviour. Note that NameSpace.valid_accesses gives different results: get_accesses ns "HOL.eq_class.eq" gives ["eq", "eq_class.eq", "HOL.eq_class.eq"] but, valid_accesses ns "HOL.eq_class.eq" gives ["HOL.eq_class.eq", "eq_class.eq", "HOL.eq", "eq"] * Patch FindTheorems: Prefer names that are shorter to type in the current context. * Re-export space_of.