1.1 --- a/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    val generate_atp_dependencies :
     1.5      Proof.context -> params -> theory -> bool -> string -> unit
     1.6    val generate_commands : Proof.context -> string -> theory -> string -> unit
     1.7 -  val generate_iter_suggestions :
     1.8 +  val generate_mepo_suggestions :
     1.9      Proof.context -> params -> theory -> int -> string -> unit
    1.10  end;
    1.11  
    1.12 @@ -182,7 +182,7 @@
    1.13      val parents = parent_facts thy thy_map
    1.14    in fold do_fact new_facts parents; () end
    1.15  
    1.16 -fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant
    1.17 +fun generate_mepo_suggestions ctxt (params as {provers, ...}) thy max_relevant
    1.18                                file_name =
    1.19    let
    1.20      val path = file_name |> Path.explode