# HG changeset patch
# User blanchet
# Date 1404059424 -7200
# Node ID 6ea8b8592787fba8d26cbc6995f8cd69f27cf4f3
# Parent  7e55bd4f9b0e6b7c2bb31fd1aa89f9cca8e1bab2
use SMT2

diff -r 7e55bd4f9b0e -r 6ea8b8592787 src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Jun 29 18:28:27 2014 +0200
+++ b/src/HOL/ROOT	Sun Jun 29 18:30:24 2014 +0200
@@ -665,7 +665,6 @@
   theories
     ATP_Theory_Export
     MaSh_Eval
-    MaSh_Export
     TPTP_Interpret
     THF_Arith
     TPTP_Proof_Reconstruction
diff -r 7e55bd4f9b0e -r 6ea8b8592787 src/HOL/TPTP/MaSh_Eval.thy
--- a/src/HOL/TPTP/MaSh_Eval.thy	Sun Jun 29 18:28:27 2014 +0200
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Sun Jun 29 18:30:24 2014 +0200
@@ -5,7 +5,7 @@
 header {* MaSh Evaluation Driver *}
 
 theory MaSh_Eval
-imports Complex_Main
+imports MaSh_Export
 begin
 
 ML_file "mash_eval.ML"
diff -r 7e55bd4f9b0e -r 6ea8b8592787 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Sun Jun 29 18:28:27 2014 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Sun Jun 29 18:30:24 2014 +0200
@@ -125,13 +125,12 @@
               in
                 Config.put atp_dest_dir dir
                 #> Config.put atp_problem_prefix (prob_prefix ^ "__")
-                #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
+                #> Config.put SMT2_Config.debug_files (dir ^ "/" ^ prob_prefix)
               end
             | set_file_name _ NONE = I
 
           fun prove method suggs =
-            if not (member (op =) methods method) orelse
-               (null facts andalso method <> IsarN) then
+            if not (member (op =) methods method) orelse (null facts andalso method <> IsarN) then
               (str_of_method method ^ "Skipped", 0)
             else
               let
@@ -146,8 +145,7 @@
                   |> take (the max_facts)
                   |> map fact_of_raw_fact
                 val ctxt = ctxt |> set_file_name method prob_dir_name
-                val res as {outcome, ...} =
-                  run_prover_for_mash ctxt params prover name facts goal
+                val res as {outcome, ...} = run_prover_for_mash ctxt params prover name facts goal
                 val ok = if is_none outcome then 1 else 0
               in
                 (str_of_result method facts res, ok)
@@ -170,9 +168,8 @@
         zeros
 
     fun total_of method ok n =
-      str_of_method method ^ string_of_int ok ^ " (" ^
-      Real.fmt (StringCvt.FIX (SOME 1))
-               (100.0 * Real.fromInt ok / Real.fromInt (Int.max (1, n))) ^ "%)"
+      str_of_method method ^ string_of_int ok ^ " (" ^ Real.fmt (StringCvt.FIX (SOME 1))
+        (100.0 * Real.fromInt ok / Real.fromInt (Int.max (1, n))) ^ "%)"
 
     val inst_inducts = Config.get ctxt instantiate_inducts
     val options =