equal
deleted
inserted
replaced
260 |
260 |
261 fun count_term (ATerm ((s, _), tms)) = |
261 fun count_term (ATerm ((s, _), tms)) = |
262 (if is_atp_variable s then I |
262 (if is_atp_variable s then I |
263 else Symtab.map_entry s (Integer.add 1)) |
263 else Symtab.map_entry s (Integer.add 1)) |
264 #> fold count_term tms |
264 #> fold count_term tms |
265 val count_formula = fold_formula count_term |
265 fun count_formula x = fold_formula count_term x |
266 |
266 |
267 val init_counters = |
267 val init_counters = |
268 metis_helpers |> map fst |> sort_distinct string_ord |> map (rpair 0) |
268 metis_helpers |> map fst |> sort_distinct string_ord |> map (rpair 0) |
269 |> Symtab.make |
269 |> Symtab.make |
270 |
270 |