# HG changeset patch
# User blanchet
# Date 1403808574 -7200
# Node ID a8eaa0e7d439a4b90b6e60651ecd2d63a4f87db6
# Parent  2b6fe2a483528e633f1311120e4ee9c2c23b17c7
tuning

diff -r 2b6fe2a48352 -r a8eaa0e7d439 src/HOL/TPTP/mash_export.ML
--- 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