# HG changeset patch
# User wenzelm
# Date 1369589252 -7200
# Node ID 576aceb343dc9c656f9975c8686584e9a4c5e19b
# Parent  761c325a65d4f68db037a943a2eb100dc7b152a5
tuned signature;

diff -r 761c325a65d4 -r 576aceb343dc src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun May 26 19:11:52 2013 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun May 26 19:27:32 2013 +0200
@@ -28,7 +28,6 @@
   val set_defsort: sort -> Proof.context -> Proof.context
   val default_sort: Proof.context -> indexname -> sort
   val consts_of: Proof.context -> Consts.T
-  val the_const_constraint: Proof.context -> string -> typ
   val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
   val facts_of: Proof.context -> Facts.T
@@ -264,8 +263,6 @@
 fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
 
 val consts_of = #1 o #consts o rep_data;
-val the_const_constraint = Consts.the_constraint o consts_of;
-
 val facts_of = #facts o rep_data;
 val cases_of = #cases o rep_data;