# HG changeset patch
# User wenzelm
# Date 1172517292 -3600
# Node ID 4d8a9e3a29f89b3cec0137fd2ec9b39fc278ab61
# Parent  914b5a0b61be29f270c542f572d265cf90df0f41
added theorems_of;

diff -r 914b5a0b61be -r 4d8a9e3a29f8 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Feb 26 20:14:47 2007 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Feb 26 20:14:52 2007 +0100
@@ -20,6 +20,7 @@
   val const_syntax_name: Proof.context -> string -> string
   val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
+  val theorems_of: Proof.context -> thm list NameSpace.table
   val fact_index_of: Proof.context -> FactIndex.T
   val transfer: theory -> Proof.context -> Proof.context
   val theory: (theory -> theory) -> Proof.context -> Proof.context
@@ -250,6 +251,7 @@
 val const_syntax_name = Consts.syntax_name o consts_of;
 
 val thms_of = #thms o rep_context;
+val theorems_of = #1 o thms_of;
 val fact_index_of = #2 o thms_of;
 
 val cases_of = #cases o rep_context;