added mk_const functions
authorhaftmann
Fri Mar 14 08:52:53 2008 +0100 (2008-03-14)
changeset 2626880aaf4d034be
parent 26267 ba710daf77a7
child 26269 5bb50f58a113
added mk_const functions
src/Pure/Isar/proof_context.ML
src/Pure/ML/ml_context.ML
src/Pure/sign.ML
     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;
     2.1 --- a/src/Pure/ML/ml_context.ML	Fri Mar 14 08:52:52 2008 +0100
     2.2 +++ b/src/Pure/ML/ml_context.ML	Fri Mar 14 08:52:53 2008 +0100
     2.3 @@ -257,8 +257,7 @@
     2.4      >> (fn ((ctxt, c), Ts) =>
     2.5        let
     2.6          val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c);
     2.7 -        val T = Consts.instance (ProofContext.consts_of ctxt) (c, Ts);
     2.8 -      in ML_Syntax.atomic (ML_Syntax.print_term (Const (c, T))) end));
     2.9 +      in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));
    2.10  
    2.11  in val _ = () end;
    2.12  
     3.1 --- a/src/Pure/sign.ML	Fri Mar 14 08:52:52 2008 +0100
     3.2 +++ b/src/Pure/sign.ML	Fri Mar 14 08:52:53 2008 +0100
     3.3 @@ -95,6 +95,7 @@
     3.4    val const_syntax_name: theory -> string -> string
     3.5    val const_typargs: theory -> string * typ -> typ list
     3.6    val const_instance: theory -> string * typ list -> typ
     3.7 +  val mk_const: theory -> string * typ list -> term
     3.8    val class_space: theory -> NameSpace.T
     3.9    val type_space: theory -> NameSpace.T
    3.10    val const_space: theory -> NameSpace.T
    3.11 @@ -264,6 +265,8 @@
    3.12  val const_typargs = Consts.typargs o consts_of;
    3.13  val const_instance = Consts.instance o consts_of;
    3.14  
    3.15 +fun mk_const thy (c, Ts) = Const (c, const_instance thy (c, Ts));
    3.16 +
    3.17  val declared_tyname = Symtab.defined o #2 o #types o Type.rep_tsig o tsig_of;
    3.18  val declared_const = can o the_const_constraint;
    3.19