changeset 33243 | 17014b1b9353 |
parent 33227 | 83322d668601 |
child 33305 | a103fa7c19cc |
--- a/src/HOL/Tools/metis_tools.ML Tue Oct 27 17:19:31 2009 +0100 +++ b/src/HOL/Tools/metis_tools.ML Tue Oct 27 17:34:00 2009 +0100 @@ -589,7 +589,7 @@ (* ------------------------------------------------------------------------- *) type logic_map = - {axioms : (Metis.Thm.thm * Thm.thm) list, + {axioms : (Metis.Thm.thm * thm) list, tfrees : ResClause.type_literal list}; fun const_in_metis c (pred, tm_list) =