# 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;