changeset 58922 | 1f500b18c4c6 |
parent 58205 | 369513534627 |
child 59058 | a78612c67ec0 |
--- a/src/HOL/TPTP/mash_eval.ML Thu Nov 06 15:05:15 2014 +0100 +++ b/src/HOL/TPTP/mash_eval.ML Thu Nov 06 15:42:34 2014 +0100 @@ -53,7 +53,7 @@ val liness' = Ctr_Sugar_Util.transpose (map pad liness0) val css = clasimpset_rule_table_of ctxt - val facts = all_facts ctxt true false Symtab.empty [] [] css + val facts = all_facts ctxt true false Keyword.empty_keywords [] [] css val name_tabs = build_name_tables nickname_of_thm facts fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)