--- a/src/HOL/TPTP/mash_eval.ML Sat Jun 28 22:13:23 2014 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Sun Jun 29 18:28:27 2014 +0200
@@ -29,6 +29,7 @@
open Sledgehammer_Prover
open Sledgehammer_Prover_ATP
open Sledgehammer_Commands
+open MaSh_Export
val prefix = Library.prefix
@@ -38,9 +39,6 @@
val MeSh_ProverN = MeShN ^ "-Prover"
val IsarN = "Isar"
-fun in_range (from, to) j =
- j >= from andalso (to = NONE orelse j <= the to)
-
fun evaluate_mash_suggestions ctxt params range methods prob_dir_name mepo_file_name
mash_isar_file_name mash_prover_file_name mesh_isar_file_name mesh_prover_file_name
report_file_name =