# HG changeset patch
# User wenzelm
# Date 937927490 -7200
# Node ID 1b977741f5302c87f796a4e715640f4422b63f3d
# Parent  f3e78ebcf6baab06681e64588cf2986599fa071b
export prems_of;

diff -r f3e78ebcf6ba -r 1b977741f530 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Sep 21 17:24:35 1999 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Sep 21 17:24:50 1999 +0200
@@ -11,6 +11,7 @@
   exception CONTEXT of string * context
   val theory_of: context -> theory
   val sign_of: context -> Sign.sg
+  val prems_of: context -> thm list
   val show_hyps: bool ref
   val pretty_thm: thm -> Pretty.T
   val verbose: bool ref