author | blanchet |
Fri, 03 Aug 2012 17:56:35 +0200 | |
changeset 48666 | 0ba2e9be9f20 |
parent 48665 | 14b0732c72f7 |
child 48667 | ac58317ef11f |
--- a/src/HOL/TPTP/mash_export.ML Fri Aug 03 17:56:35 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Fri Aug 03 17:56:35 2012 +0200 @@ -152,7 +152,8 @@ val core = escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^ escape_metas feats - val query = if kind <> "" then "? " ^ core ^ "\n" else "" + val query = + if kind = "" orelse null deps then "" else "? " ^ core ^ "\n" val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n" val _ = File.append path (query ^ update) in [name] end