src/HOL/TPTP/mash_eval.ML

     val sugg_path = sugg_file_name |> Path.explode
     val lines = sugg_path |> File.read_lines
     val css = clasimpset_rule_table_of ctxt
     val facts = all_facts ctxt true false Symtab.empty [] [] css
     val all_names = build_all_names nickname_of facts
-    val mepo_ok = Unsynchronized.ref 0
-    val mash_ok = Unsynchronized.ref 0
-    val mesh_ok = Unsynchronized.ref 0
-    val isar_ok = Unsynchronized.ref 0
+    val mepo_ok = Synchronized.var "mepo_ok" 0
+    val mash_ok = Synchronized.var "mash_ok" 0
+    val mesh_ok = Synchronized.var "mesh_ok" 0
+    val isar_ok = Synchronized.var "isar_ok" 0
     fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
     fun index_string (j, s) = s ^ "@" ^ string_of_int j
     fun str_of_res label facts ({outcome, run_time, used_facts, ...}
                                 : prover_result) =
       let val facts = facts |> map (fn ((name, _), _) => name ()) in

                 |> maybe_instantiate_inducts ctxt hyp_ts concl_t
                 |> take (the max_facts)
               val ctxt = ctxt |> set_file_name heading prob_dir_name
               val res as {outcome, ...} =
                 run_prover_for_mash ctxt params prover facts goal
-              val _ = if is_none outcome then ok := !ok + 1 else ()
+              val _ =
+                if is_none outcome then Synchronized.change ok (Integer.add 1)
+                else ()
             in str_of_res heading facts res end
           val [mepo_s, mash_s, mesh_s, isar_s] =
             [fn () => prove mepo_ok MePoN fst mepo_facts,
              fn () => prove mash_ok MaShN fst mash_facts,
              fn () => prove mesh_ok MeShN I mesh_facts,
              fn () => prove isar_ok IsarN fst isar_facts]
             |> (* Par_List. *) map (fn f => f ())
         in
           ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
            isar_s]
-          |> cat_lines |> print
+          |> cat_lines |> print;
+          1
         end
       else
-        ()
+        0
     fun total_of heading ok n =
-      "  " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
-      Real.fmt (StringCvt.FIX (SOME 1))
-               (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
+      let val ok_val = Synchronized.value ok in
+        "  " ^ heading ^ ": " ^ string_of_int ok_val ^ " (" ^
+        Real.fmt (StringCvt.FIX (SOME 1))
+                 (100.0 * Real.fromInt ok_val / Real.fromInt n) ^ "%)"
+      end
     val inst_inducts = Config.get ctxt instantiate_inducts
     val options =
       [prover, string_of_int (the max_facts) ^ " facts",
        "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
        the_default "smart" lam_trans,
        ATP_Util.string_from_time (timeout |> the_default one_year),
        "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
-    val n = length lines
+    val _ = print " * * *";
+    val _ = print ("Options: " ^ commas options);
+    val n = Integer.sum (Par_List.map solve_goal (tag_list 1 lines))
   in
-    print " * * *";
-    print ("Options: " ^ commas options);
-    Par_List.map solve_goal (tag_list 1 lines);
     ["Successes (of " ^ string_of_int n ^ " goals)",
      total_of MePoN mepo_ok n,
      total_of MaShN mash_ok n,
      total_of MeShN mesh_ok n,
      total_of IsarN isar_ok n]