prim_mk_const
Term.prim_mk_const : {Thy:string, Name:string} -> term
Build a constant.
If Name is the name of a previously declared constant in theory Thy,
then prim_mk_const {Thy,Name} will return the specified constant.
Failure
If Name is not the name of a constant declared in theory Thy.
Example
> prim_mk_const {Thy="min", Name="="};
val it = “$=”: term
> type_of it;
val it = “:α -> α -> bool”: hol_type
Comments
The difference between mk_thy_const (and mk_const) and
prim_mk_const is that mk_thy_const and mk_const will create type
instances of polymorphic constants, while prim_mk_const merely returns
the originally declared constant.