# HG changeset patch # User wenzelm # Date 1208375581 -7200 # Node ID 90d0b86644ac215a36259f0103a9c6871f590795 # Parent 3f48d4f4229f4c0c98b1bf0971a55998589e6e76 renamed check_fact to defined_fact; diff -r 3f48d4f4229f -r 90d0b86644ac src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Wed Apr 16 21:53:00 2008 +0200 +++ b/src/Pure/pure_thy.ML Wed Apr 16 21:53:01 2008 +0200 @@ -25,7 +25,7 @@ val has_internal: Markup.property list -> bool val is_internal: thm -> bool val intern_fact: theory -> xstring -> string - val check_fact: theory -> string -> bool + val defined_fact: theory -> string -> bool val get_fact: Context.generic -> theory -> Facts.ref -> thm list val get_thms: theory -> xstring -> thm list val get_thm: theory -> xstring -> thm @@ -149,7 +149,7 @@ val facts_of = #all_facts o get_theorems; val intern_fact = Facts.intern o facts_of; -fun check_fact thy name = is_some (Facts.lookup (Context.Theory thy) (facts_of thy) name); +val defined_fact = Facts.defined o facts_of;