src/Pure/Isar/proof_context.ML
changeset 26268 80aaf4d034be
parent 26250 96035b40be60
child 26284 533dcb120a8e
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Mar 14 08:52:52 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Mar 14 08:52:53 2008 +0100
     1.3 @@ -26,6 +26,7 @@
     1.4    val consts_of: Proof.context -> Consts.T
     1.5    val const_syntax_name: Proof.context -> string -> string
     1.6    val the_const_constraint: Proof.context -> string -> typ
     1.7 +  val mk_const: Proof.context -> string * typ list -> term
     1.8    val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
     1.9    val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
    1.10    val theorems_of: Proof.context -> thm list NameSpace.table
    1.11 @@ -255,6 +256,8 @@
    1.12  val const_syntax_name = Consts.syntax_name o consts_of;
    1.13  val the_const_constraint = Consts.the_constraint o consts_of;
    1.14  
    1.15 +fun mk_const ctxt (c, Ts) = Const (c, Consts.instance (consts_of ctxt) (c, Ts));
    1.16 +
    1.17  val thms_of = #thms o rep_context;
    1.18  val theorems_of = #1 o thms_of;
    1.19  val fact_index_of = #2 o thms_of;