src/Pure/Isar/proof_context.ML

   val syn_of: Proof.context -> Syntax.syntax
   val tsig_of: Proof.context -> Type.tsig
   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
   val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
   val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context

 val tsig_of = #1 o #tsig o rep_data;
 val set_defsort = map_tsig o apfst o Type.set_defsort;
 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;
 
 
 (* naming *)