equal
deleted
inserted
replaced
587 (* ------------------------------------------------------------------------- *) |
587 (* ------------------------------------------------------------------------- *) |
588 (* Logic maps manage the interface between HOL and first-order logic. *) |
588 (* Logic maps manage the interface between HOL and first-order logic. *) |
589 (* ------------------------------------------------------------------------- *) |
589 (* ------------------------------------------------------------------------- *) |
590 |
590 |
591 type logic_map = |
591 type logic_map = |
592 {axioms : (Metis.Thm.thm * Thm.thm) list, |
592 {axioms : (Metis.Thm.thm * thm) list, |
593 tfrees : ResClause.type_literal list}; |
593 tfrees : ResClause.type_literal list}; |
594 |
594 |
595 fun const_in_metis c (pred, tm_list) = |
595 fun const_in_metis c (pred, tm_list) = |
596 let |
596 let |
597 fun in_mterm (Metis.Term.Var _) = false |
597 fun in_mterm (Metis.Term.Var _) = false |