equal
deleted
inserted
replaced
426 term_contains1 (NONE::Bs, FVs) t t2 |
426 term_contains1 (NONE::Bs, FVs) t t2 |
427 |
427 |
428 | term_contains1 T (ah $ at) (bh $ bt) = |
428 | term_contains1 T (ah $ at) (bh $ bt) = |
429 (term_contains1 T ah (bh $ bt)) @ |
429 (term_contains1 T ah (bh $ bt)) @ |
430 (term_contains1 T at (bh $ bt)) @ |
430 (term_contains1 T at (bh $ bt)) @ |
431 (List.concat (map (fn inT => (term_contains1 inT at bt)) |
431 (maps (fn inT => (term_contains1 inT at bt)) (term_contains1 T ah bh)) |
432 (term_contains1 T ah bh))) |
|
433 |
432 |
434 | term_contains1 T a (bh $ bt) = [] |
433 | term_contains1 T a (bh $ bt) = [] |
435 |
434 |
436 | term_contains1 T (ah $ at) b = |
435 | term_contains1 T (ah $ at) b = |
437 (term_contains1 T ah b) @ (term_contains1 T at b) |
436 (term_contains1 T ah b) @ (term_contains1 T at b) |