src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

   string_of_int (length (Graph.maximals G)) ^ " maximal"
 
 type mash_state =
   {access_G : (proof_kind * string list * string list) Graph.T,
    num_known_facts : int,
-   dirty : string list option}
-
-val empty_state = {access_G = Graph.empty, num_known_facts = 0, dirty = SOME []} : mash_state
+   dirty_facts : string list option}
+
+val empty_state = {access_G = Graph.empty, num_known_facts = 0, dirty_facts = SOME []} : mash_state
 
 local
 
 val version = "*** MaSh version 20140625 ***"
 

                   else wipe_out_mash_state_dir ();
                   (Graph.empty, 0))
                | GREATER => raise FILE_VERSION_TOO_NEW ())
            in
              trace_msg ctxt (fn () => "Loaded fact graph (" ^ graph_info access_G ^ ")");
-             {access_G = access_G, num_known_facts = num_known_facts, dirty = SOME []}
+             {access_G = access_G, num_known_facts = num_known_facts, dirty_facts = SOME []}
            end
          | _ => empty_state)))
   end
 
 fun str_of_entry (kind, name, parents, feats, deps) =
   str_of_proof_kind kind ^ " " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
   encode_strs feats ^ "; " ^ encode_strs deps ^ "\n"
 
-fun save_state _ (time_state as (_, {dirty = SOME [], ...})) = time_state
-  | save_state ctxt (memory_time, {access_G, num_known_facts, dirty}) =
+fun save_state _ (time_state as (_, {dirty_facts = SOME [], ...})) = time_state
+  | save_state ctxt (memory_time, {access_G, num_known_facts, dirty_facts}) =
     let
       fun append_entry (name, ((kind, feats, deps), (parents, _))) =
         cons (kind, name, Graph.Keys.dest parents, feats, deps)
 
       val path = mash_state_file ()
-      val dirty' =
+      val dirty_facts' =
         (case try OS.FileSys.modTime (Path.implode path) of
           NONE => NONE
-        | SOME disk_time => if Time.< (disk_time, memory_time) then dirty else NONE)
+        | SOME disk_time => if Time.< (disk_time, memory_time) then dirty_facts else NONE)
       val (banner, entries) =
-        (case dirty' of
+        (case dirty_facts' of
           SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names [])
         | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G []))
     in
       write_file banner (entries, str_of_entry) path;
       trace_msg ctxt (fn () =>
         "Saved fact graph (" ^ graph_info access_G ^
-        (case dirty of
-          SOME dirty => "; " ^ string_of_int (length dirty) ^ " dirty fact(s)"
+        (case dirty_facts of
+          SOME dirty_facts => "; " ^ string_of_int (length dirty_facts) ^ " dirty fact(s)"
         | _ => "") ^  ")");
-      (Time.now (), {access_G = access_G, num_known_facts = num_known_facts, dirty = SOME []})
+      (Time.now (), {access_G = access_G, num_known_facts = num_known_facts, dirty_facts = SOME []})
     end
 
-val global_state =
-  Synchronized.var "Sledgehammer_MaSh.global_state" (Time.zeroTime, empty_state)
+val global_state = Synchronized.var "Sledgehammer_MaSh.global_state" (Time.zeroTime, empty_state)
 
 in
 
 fun map_state ctxt overlord f =
   Synchronized.change global_state (load_state ctxt overlord ##> f #> save_state ctxt)

     launch_thread timeout (fn () =>
       let
         val thy = Proof_Context.theory_of ctxt
         val feats = map fst (features_of ctxt thy 0 Symtab.empty (Local, General) [t])
       in
-        map_state ctxt overlord (fn state as {access_G, num_known_facts, dirty} =>
+        map_state ctxt overlord (fn state as {access_G, num_known_facts, dirty_facts} =>
           let
             val parents = maximal_wrt_access_graph access_G facts
             val deps = used_ths
               |> filter (is_fact_in_graph access_G)
               |> map nickname_of_thm

               let
                 val name = learned_proof_name ()
                 val access_G = access_G |> add_node Automatic_Proof name parents feats deps
               in
                 {access_G = access_G, num_known_facts = num_known_facts + 1,
-                 dirty = Option.map (cons name) dirty}
+                 dirty_facts = Option.map (cons name) dirty_facts}
               end
           end);
         (true, "")
       end)
   else

             |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps)
           else
             isar_dependencies_of name_tabs th
 
         fun do_commit [] [] [] state = state
-          | do_commit learns relearns flops {access_G, num_known_facts, dirty} =
+          | do_commit learns relearns flops {access_G, num_known_facts, dirty_facts} =
             let
               val was_empty = Graph.is_empty access_G
               val (learns, access_G) = ([], access_G) |> fold (learn_wrt_access_graph ctxt) learns
               val (relearns, access_G) =
                 ([], access_G) |> fold (relearn_wrt_access_graph ctxt) relearns
               val access_G = access_G |> fold flop_wrt_access_graph flops
               val num_known_facts = num_known_facts + length learns
-              val dirty =
-                (case (was_empty, dirty) of
+              val dirty_facts =
+                (case (was_empty, dirty_facts) of
                   (false, SOME names) => SOME (map #1 learns @ map #1 relearns @ names)
                 | _ => NONE)
             in
               if engine = MaSh_Py then
                 (MaSh_Py.learn ctxt overlord (save andalso null relearns) (rev learns);
                  MaSh_Py.relearn ctxt overlord save relearns)
               else
                 ();
-              {access_G = access_G, num_known_facts = num_known_facts, dirty = dirty}
+              {access_G = access_G, num_known_facts = num_known_facts, dirty_facts = dirty_facts}
             end
 
         fun commit last learns relearns flops =
           (if debug andalso auto_level = 0 then Output.urgent_message "Committing..." else ();
            map_state ctxt overlord (do_commit (rev learns) relearns flops);