1.1 --- a/src/HOL/TPTP/mash_export.ML	Thu Jun 26 20:32:31 2014 +0200
     1.2 +++ b/src/HOL/TPTP/mash_export.ML	Thu Jun 26 20:49:34 2014 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4  
     1.5  fun generate_features ctxt thys file_name =
     1.6    let
     1.7 -    val path = file_name |> Path.explode
     1.8 +    val path = Path.explode file_name
     1.9      val _ = File.write path ""
    1.10      val facts = all_facts ctxt |> filter_out (has_thys thys o snd)
    1.11  
    1.12 @@ -158,7 +158,7 @@
    1.13  fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name =
    1.14    let
    1.15      val ho_atp = is_ho_atp ctxt prover
    1.16 -    val path = file_name |> Path.explode
    1.17 +    val path = Path.explode file_name
    1.18      val facts = all_facts ctxt
    1.19      val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
    1.20      val num_old_facts = length old_facts
    1.21 @@ -228,7 +228,7 @@
    1.22      (params as {provers = prover :: _, ...}) (range, step) thys max_suggs file_name =
    1.23    let
    1.24      val ho_atp = is_ho_atp ctxt prover
    1.25 -    val path = file_name |> Path.explode
    1.26 +    val path = Path.explode file_name
    1.27      val facts = all_facts ctxt
    1.28      val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
    1.29      val name_tabs = build_name_tables nickname_of_thm facts