1\DOC mk_thy_const 2 3\TYPE {mk_thy_const : {Thy:string, Name:string, Ty:hol_type} -> term} 4 5\SYNOPSIS 6Constructs a constant. 7 8\DESCRIBE 9If {n} is a string that has been previously declared to be a constant 10with type {ty} in theory {thy}, and {ty1} is an instance of {ty}, 11then {mk_thy_const{Name=n, Thy=thy, Ty=ty1}} returns the specified 12instance of the constant. 13 14(A type {ty1} is an 'instance' of a type {ty2} when {match_type ty2 ty1} 15does not fail.) 16 17\FAILURE 18Fails if {n} is not the name of a constant in theory {thy}, if {thy} is 19not in the ancestry of the current theory, or if {ty1} is not an 20instance of {ty}. 21 22\EXAMPLE 23{ 24 - mk_thy_const {Name="T", Thy="bool", Ty=bool}; 25 > val it = `T` : term 26 27 - try mk_thy_const {Name = "bar", Thy="foo", Ty=bool}; 28 Exception raised at Term.mk_thy_const: 29 "foo$bar" not found 30} 31 32 33\SEEALSO 34Term.dest_thy_const, Term.mk_const, Term.dest_const, Term.is_const, Term.mk_var, Term.mk_comb, Term.mk_abs, Type.match_type. 35\ENDDOC 36