equal
deleted
inserted
replaced
87 | add_line_pass1 line lines = line :: lines |
87 | add_line_pass1 line lines = line :: lines |
88 |
88 |
89 fun add_lines_pass2 res [] = rev res |
89 fun add_lines_pass2 res [] = rev res |
90 | add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) = |
90 | add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) = |
91 let |
91 let |
|
92 val line as (name, role, t, rule, deps) = (name, role, Term.map_aterms |
|
93 (perhaps (try (fn Free (s, T) => Free (unsuffix "__" s, T)))) t |
|
94 |> Term.map_abs_vars (perhaps (try (unsuffix "__"))), rule, deps) (*###*) |
92 val is_last_line = null lines |
95 val is_last_line = null lines |
93 |
96 |
94 fun looks_interesting () = |
97 fun looks_interesting () = |
95 not (is_True_prop t) andalso null (Term.add_tvars t []) andalso length deps >= 2 andalso |
98 not (is_True_prop t) andalso null (Term.add_tvars t []) andalso length deps >= 2 andalso |
96 not (can the_single lines) |
99 not (can the_single lines) |