# HG changeset patch
# User wenzelm
# Date 1172517287 -3600
# Node ID 914b5a0b61be29f270c542f572d265cf90df0f41
# Parent  fe054a72d9ce95a12e09da45ebe2ced6a13437cf
removed obsolete theorem_space;

diff -r fe054a72d9ce -r 914b5a0b61be src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Feb 26 15:08:37 2007 +0100
+++ b/src/Pure/pure_thy.ML	Mon Feb 26 20:14:47 2007 +0100
@@ -50,7 +50,6 @@
   val select_thm: thmref -> thm list -> thm list
   val selections: string * thm list -> (thmref * thm) list
   val theorems_of: theory -> thm list NameSpace.table
-  val theorem_space: theory -> NameSpace.T
   val fact_index_of: theory -> FactIndex.T
   val valid_thms: theory -> thmref * thm list -> bool
   val thms_containing: theory -> FactIndex.spec -> (string * thm list) list
@@ -171,7 +170,6 @@
 val get_theorems_ref = TheoremsData.get;
 val get_theorems = ! o get_theorems_ref;
 val theorems_of = #theorems o get_theorems;
-val theorem_space = #1 o theorems_of;
 val fact_index_of = #index o get_theorems;