changeset 48296 | e7f01b7e244e |
parent 48292 | 7fcee834c7f5 |
child 48299 | 5e5c6616f0fe |
--- a/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:03 2012 +0200 @@ -43,7 +43,7 @@ val _ = File.append path (query ^ update) in [name] end val thy_ths = old_facts |> thms_by_thy - val parents = parent_thms thy_ths thy + val parents = parent_facts thy_ths thy in fold do_fact new_facts parents; () end fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant