added const_instance;
authorwenzelm
Mon Nov 14 14:37:48 2005 +0100 (2005-11-14)
changeset 18164eb4206c930cd
parent 18163 9b729737bf14
child 18165 cbed396ecb1c
added const_instance;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Mon Nov 14 14:37:38 2005 +0100
     1.2 +++ b/src/Pure/sign.ML	Mon Nov 14 14:37:48 2005 +0100
     1.3 @@ -115,6 +115,7 @@
     1.4    val declared_const: theory -> string -> bool
     1.5    val const_monomorphic: theory -> string -> bool
     1.6    val const_typargs: theory -> string * typ -> typ list
     1.7 +  val const_instance: theory -> string * typ list -> typ
     1.8    val class_space: theory -> NameSpace.T
     1.9    val type_space: theory -> NameSpace.T
    1.10    val const_space: theory -> NameSpace.T
    1.11 @@ -280,6 +281,7 @@
    1.12  val const_type = try o the_const_type;
    1.13  val const_monomorphic = Consts.monomorphic o consts_of;
    1.14  val const_typargs = Consts.typargs o consts_of;
    1.15 +val const_instance = Consts.instance o consts_of;
    1.16  
    1.17  val declared_tyname = Symtab.defined o #2 o #types o Type.rep_tsig o tsig_of;
    1.18  val declared_const = is_some oo const_type;