added mk_const functions

--- a/src/Pure/Isar/proof_context.ML	Fri Mar 14 08:52:52 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Mar 14 08:52:53 2008 +0100
@@ -26,6 +26,7 @@
   val consts_of: Proof.context -> Consts.T
   val const_syntax_name: Proof.context -> string -> string
   val the_const_constraint: Proof.context -> string -> typ
+  val mk_const: Proof.context -> string * typ list -> term
   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
@@ -255,6 +256,8 @@
 val const_syntax_name = Consts.syntax_name o consts_of;
 val the_const_constraint = Consts.the_constraint o consts_of;
 
+fun mk_const ctxt (c, Ts) = Const (c, Consts.instance (consts_of ctxt) (c, Ts));
+
 val thms_of = #thms o rep_context;
 val theorems_of = #1 o thms_of;
 val fact_index_of = #2 o thms_of;

--- a/src/Pure/ML/ml_context.ML	Fri Mar 14 08:52:52 2008 +0100
+++ b/src/Pure/ML/ml_context.ML	Fri Mar 14 08:52:53 2008 +0100
@@ -257,8 +257,7 @@
     >> (fn ((ctxt, c), Ts) =>
       let
         val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c);
-        val T = Consts.instance (ProofContext.consts_of ctxt) (c, Ts);
-      in ML_Syntax.atomic (ML_Syntax.print_term (Const (c, T))) end));
+      in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));
 
 in val _ = () end;
 

--- a/src/Pure/sign.ML	Fri Mar 14 08:52:52 2008 +0100
+++ b/src/Pure/sign.ML	Fri Mar 14 08:52:53 2008 +0100
@@ -95,6 +95,7 @@
   val const_syntax_name: theory -> string -> string
   val const_typargs: theory -> string * typ -> typ list
   val const_instance: theory -> string * typ list -> typ
+  val mk_const: theory -> string * typ list -> term
   val class_space: theory -> NameSpace.T
   val type_space: theory -> NameSpace.T
   val const_space: theory -> NameSpace.T
@@ -264,6 +265,8 @@
 val const_typargs = Consts.typargs o consts_of;
 val const_instance = Consts.instance o consts_of;
 
+fun mk_const thy (c, Ts) = Const (c, const_instance thy (c, Ts));
+
 val declared_tyname = Symtab.defined o #2 o #types o Type.rep_tsig o tsig_of;
 val declared_const = can o the_const_constraint;