mk_thy_const : {Thy:string, Name:string, Ty:hol_type} -> term
STRUCTURE
Term
SYNOPSIS
Constructs a constant.
DESCRIPTION
If n is a string that has been previously declared to be a constant with type ty in theory thy, and ty1 is an instance of ty, then mk_thy_const{Name=n, Thy=thy, Ty=ty1} returns the specified instance of the constant.

(A type ty1 is an ’instance’ of a type ty2 when match_type ty2 ty1 does not fail.)

FAILURE
Fails if n is not the name of a constant in theory thy, if thy is not in the ancestry of the current theory, or if ty1 is not an instance of ty.
EXAMPLE
   - mk_thy_const {Name="T", Thy="bool", Ty=bool};
   > val it = `T` : term

   - try mk_thy_const {Name = "bar", Thy="foo", Ty=bool};
   Exception raised at Term.mk_thy_const:
   "foo$bar" not found

SEEALSO
dest_thy_const, mk_const, dest_const, is_const, mk_var, mk_comb, mk_abs, match_type
HOL  Kananaskis-13