diff -r dd9decc0bb6d -r bcadd6e7739c src/Pure/fact_index.ML
--- a/src/Pure/fact_index.ML	Tue Jul 04 21:22:50 2006 +0200
+++ b/src/Pure/fact_index.ML	Tue Jul 04 21:22:51 2006 +0200
@@ -10,6 +10,7 @@
   type spec
   type T
   val facts: T -> (string * thm list) list
+  val props: T -> thm list
   val could_unify: T -> term -> thm list
   val empty: T
   val add_global: (string * thm list) -> T -> T
@@ -53,6 +54,8 @@
   props: thm Net.net};
 
 fun facts (Index {facts, ...}) = facts;
+fun props (Index {props, ...}) =
+  sort_distinct (Term.term_ord o pairself Thm.full_prop_of) (Net.content props);
 fun could_unify (Index {props, ...}) = Net.unify_term props;
 
 val empty =