Lines Matching defs:ts
146 val (_, ts) = strip_comb t
147 val ts' = tl ts
148 val _ = if is_var (hd ts) andalso not (null ts') then () else fail()
149 val ts'' = map (snd o strip_abs) ts'
150 val ds = List.foldl (fn (t, s) => s + average_tree_depth t) 0.0 ts''
151 val ds' = (ds / (real (length ts''))) + 1.0
273 fun pr ts = let
274 val ts_sl = List.map (fn t => "``" ^ (Hol_pp.term_to_string t) ^ "``") ts