equal
deleted
inserted
replaced
181 if polymorphism_of_type_enc type_enc = Polymorphic then |
181 if polymorphism_of_type_enc type_enc = Polymorphic then |
182 (conj_clauses, fact_clauses) |
182 (conj_clauses, fact_clauses) |
183 else |
183 else |
184 conj_clauses @ fact_clauses |
184 conj_clauses @ fact_clauses |
185 |> map (pair 0) |
185 |> map (pair 0) |
186 |> rpair ctxt |
186 |> rpair (ctxt |> Config.put Monomorph.keep_partial_instances false) |
187 |-> Monomorph.monomorph atp_schematic_consts_of |
187 |-> Monomorph.monomorph atp_schematic_consts_of |
188 |> fst |> chop (length conj_clauses) |
188 |> fst |> chop (length conj_clauses) |
189 |> pairself (maps (map (zero_var_indexes o snd))) |
189 |> pairself (maps (map (zero_var_indexes o snd))) |
190 val num_conjs = length conj_clauses |
190 val num_conjs = length conj_clauses |
191 val clauses = |
191 val clauses = |