Lines Matching defs:used
94 val used = usedNTs g
98 val used_less_defined = HOLset.difference(used, defined)
318 fun sym_to_term nty (gi as {tokmap,tokty,mkntname,...}:ginfo) sym used = let
327 fun var aty used = let
328 val t = variant used (mk_var(appletter aty, aty))
330 (t::used, Some t)
332 val (used, vs) =
333 case mmap var args used of
335 | (used, Some vs) => (used, vs)
337 (used, Some (mktok (list_mk_comb(t, vs))))
341 TOK (S s) => (used, Some (mktok (tokmap s)))
343 | NT n => (used, Some (mkNT nty gi n))
378 val (used, ts) =
380 (used, Some ts) => (used, ts)
384 case used of
386 | _ => mk_icomb(gspec_tm, mk_pabs(list_mk_pair used, mk_pair(body, T)))