src/HOL/TPTP/mash_export.ML
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