Lines Matching defs:terms
86 (* finding and replacing terms *)
135 (* making and destroying terms *)
634 fun terms ([],x) = ((hd (filter frame_var xs),x) handle Empty => (list_mk_star [] (type_of (car tm1)),x))
635 | terms (((y,z)::ys),x) = let
636 val (y2,z2) = terms (ys,x)
641 val (x,y,s) = try_each (g o terms) ts
1290 fun terms ([],x) = ((hd (filter frame_var xs),x) handle Empty => (list_mk_star [] (type_of (car tm1)),x))
1291 | terms (((y,z)::ys),x) = let
1292 val (y2,z2) = terms (ys,x)
1295 val (x,y) = (term_full o terms) (hd ts)
1306 val _ = print "\n\n\nstar_match failed on terms:\n"