--- a/src/HOL/TPTP/mash_export.ML Thu Jun 26 20:32:31 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML Thu Jun 26 20:49:34 2014 +0200
@@ -71,7 +71,7 @@
fun generate_features ctxt thys file_name =
let
- val path = file_name |> Path.explode
+ val path = Path.explode file_name
val _ = File.write path ""
val facts = all_facts ctxt |> filter_out (has_thys thys o snd)
@@ -158,7 +158,7 @@
fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name =
let
val ho_atp = is_ho_atp ctxt prover
- val path = file_name |> Path.explode
+ val path = Path.explode file_name
val facts = all_facts ctxt
val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
val num_old_facts = length old_facts
@@ -228,7 +228,7 @@
(params as {provers = prover :: _, ...}) (range, step) thys max_suggs file_name =
let
val ho_atp = is_ho_atp ctxt prover
- val path = file_name |> Path.explode
+ val path = Path.explode file_name
val facts = all_facts ctxt
val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
val name_tabs = build_name_tables nickname_of_thm facts