220 |-> Monomorph.monomorph atp_schematic_consts_of |
220 |-> Monomorph.monomorph atp_schematic_consts_of |
221 |> fst |> chop (length conj_clauses) |
221 |> fst |> chop (length conj_clauses) |
222 |> pairself (maps (map (zero_var_indexes o snd))) |
222 |> pairself (maps (map (zero_var_indexes o snd))) |
223 val num_conjs = length conj_clauses |
223 val num_conjs = length conj_clauses |
224 val clauses = |
224 val clauses = |
225 map2 (fn j => pair (Int.toString j, Local)) |
225 map2 (fn j => pair (Int.toString j, (Local, General))) |
226 (0 upto num_conjs - 1) conj_clauses @ |
226 (0 upto num_conjs - 1) conj_clauses @ |
227 (* "General" below isn't quite correct; the fact could be local. *) |
227 map2 (fn j => pair (Int.toString (num_conjs + j), (Local, General))) |
228 map2 (fn j => pair (Int.toString (num_conjs + j), General)) |
|
229 (0 upto length fact_clauses - 1) fact_clauses |
228 (0 upto length fact_clauses - 1) fact_clauses |
230 val (old_skolems, props) = |
229 val (old_skolems, props) = |
231 fold_rev (fn (name, th) => fn (old_skolems, props) => |
230 fold_rev (fn (name, th) => fn (old_skolems, props) => |
232 th |> prop_of |> Logic.strip_imp_concl |
231 th |> prop_of |> Logic.strip_imp_concl |
233 |> conceal_old_skolem_terms (length clauses) old_skolems |
232 |> conceal_old_skolem_terms (length clauses) old_skolems |