--- 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
@@ -38,9 +38,10 @@
val kind = Thm.legacy_get_kind th
val name = fact_name_of name
val core =
- name ^ ": " ^ space_implode " " prevs ^ "; " ^ space_implode " " feats
+ space_implode " " prevs ^ "; " ^ space_implode " " feats
val query = if kind <> "" then "? " ^ core ^ "\n" else ""
- val update = "! " ^ core ^ "; " ^ space_implode " " deps ^ "\n"
+ val update =
+ "! " ^ name ^ ": " ^ core ^ "; " ^ space_implode " " deps ^ "\n"
val _ = File.append path (query ^ update)
in [name] end
val thy_ths = old_facts |> thms_by_thy