equal
deleted
inserted
replaced
277 | pred_of_sort (LTFree (s,ty)) = (s,1) |
277 | pred_of_sort (LTFree (s,ty)) = (s,1) |
278 |
278 |
279 (*Given a list of sorted type variables, return a list of type literals.*) |
279 (*Given a list of sorted type variables, return a list of type literals.*) |
280 fun add_typs Ts = foldl (op union) [] (map sorts_on_typs Ts); |
280 fun add_typs Ts = foldl (op union) [] (map sorts_on_typs Ts); |
281 |
281 |
|
282 (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear. |
|
283 * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a |
|
284 in a lemma has the same sort as 'a in the conjecture. |
|
285 * Deleting such clauses will lead to problems with locales in other use of local results |
|
286 where 'a is fixed. Probably we should delete clauses unless the sorts agree. |
|
287 * Currently we include a class constraint in the clause, exactly as with TVars. |
|
288 *) |
|
289 |
282 (** make axiom and conjecture clauses. **) |
290 (** make axiom and conjecture clauses. **) |
283 |
291 |
284 fun get_tvar_strs [] = [] |
292 fun get_tvar_strs [] = [] |
285 | get_tvar_strs ((TVar (indx,s))::Ts) = |
293 | get_tvar_strs ((TVar (indx,s))::Ts) = |
286 insert (op =) (make_schematic_type_var indx) (get_tvar_strs Ts) |
294 insert (op =) (make_schematic_type_var indx) (get_tvar_strs Ts) |