# HG changeset patch
# User haftmann
# Date 1191049137 -7200
# Node ID 8aec6154bb17362a49fc0505dffec0713ec3fa35
# Parent  dbb34a03af5aeaafe87b7dc6d123b201efb288f0
exported constraint interfaces

diff -r dbb34a03af5a -r 8aec6154bb17 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Sep 29 08:58:56 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Sep 29 08:58:57 2007 +0200
@@ -25,6 +25,9 @@
   val full_name: Proof.context -> bstring -> string
   val consts_of: Proof.context -> Consts.T
   val const_syntax_name: Proof.context -> string -> string
+  val const_constraint: Proof.context -> string -> typ option
+  val the_const_constraint: Proof.context -> string -> typ
+  val add_const_constraint: string * typ option -> Proof.context -> Proof.context
   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
@@ -266,6 +269,9 @@
 
 val consts_of = #2 o #consts o rep_context;
 val const_syntax_name = Consts.syntax_name o consts_of;
+val const_constraint = try o Consts.the_constraint o consts_of;
+val the_const_constraint = Consts.the_constraint o consts_of;
+val add_const_constraint = map_consts o apsnd o Consts.constrain;
 
 val thms_of = #thms o rep_context;
 val theorems_of = #1 o thms_of;