Lines Matching defs:con
363 (* con mlchr = fn : char -> mlsexp *)
364 (* con mlnum = fn : string * string * string * string -> mlsexp *)
365 (* con mlpair = fn : mlsexp * mlsexp -> mlsexp *)
366 (* con mlstr = fn : string -> mlsexp *)
367 (* con mlsym = fn : string * string -> mlsexp *)
1656 let val (con,tm) = dest_comb conc
1657 val _ = if not(is_const con andalso (fst(dest_const con) = "|="))
2087 val con = mk_const(opr_name,opr_ty)
2088 val newtm = subst[opr |-> con]tm
2134 (map2 (fn opr => fn con => (opr |-> con)) tms con_list)
2162 (map2 (fn opr => fn con => (opr |-> con)) tms con_list)