src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

   val relearn_isarN : string
   val relearn_proverN : string
   val fact_filters : string list
   val encode_str : string -> string
   val encode_strs : string list -> string
-  val unencode_str : string -> string
-  val unencode_strs : string -> string list
-  val encode_plain_features : string list list -> string
+  val decode_str : string -> string
+  val decode_strs : string -> string list
+  val encode_unweighted_features : string list list -> string
   val encode_features : (string list * real) list -> string
   val extract_suggestions : string -> string * string list
 
   structure MaSh:
   sig

 open Sledgehammer_Fact
 open Sledgehammer_Prover
 open Sledgehammer_Prover_Minimize
 open Sledgehammer_MePo
 
-val trace =
-  Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
+val trace = Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
 
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
 
 val MePoN = "MePo"
 val MaShN = "MaSh"

       " --modelFile=" ^ model_dir ^ "/model.pickle\
       \ --dictsFile=" ^ model_dir ^ "/dict.pickle\
       \ --log " ^ log_file ^
       " --inputFile " ^ cmd_file ^
       " --predictions " ^ sugg_file ^
-      (if extra_args = [] then "" else " " ^ space_implode " " extra_args) ^
-      " >& " ^ err_file ^
+      (if extra_args = [] then "" else " " ^ space_implode " " extra_args) ^ " >& " ^ err_file ^
       (if background then " &" else "")
     fun run_on () =
       (Isabelle_System.bash command
        |> tap (fn _ =>
             (case try File.read (Path.explode err_file) |> the_default "" of
               "" => trace_msg ctxt (K "Done")
             | s => warning ("MaSh error: " ^ elide_string 1000 s)));
        read_suggs (fn () => try File.read_lines sugg_path |> these))
     fun clean_up () =
-      if overlord then ()
-      else List.app wipe_out_file [err_file, sugg_file, cmd_file]
+      if overlord then () else List.app wipe_out_file [err_file, sugg_file, cmd_file]
   in
     write_file (SOME "") ([], K "") sugg_path;
     write_file (SOME "") write_cmds cmd_path;
     trace_msg ctxt (fn () => "Running " ^ command);
     with_cleanup clean_up run_on ()

     "%" ^ stringN_of_int 3 (Char.ord c)
 
 fun unmeta_chars accum [] = String.implode (rev accum)
   | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) =
     (case Int.fromString (String.implode [d1, d2, d3]) of
-       SOME n => unmeta_chars (Char.chr n :: accum) cs
-     | NONE => "" (* error *))
+      SOME n => unmeta_chars (Char.chr n :: accum) cs
+    | NONE => "" (* error *))
   | unmeta_chars _ (#"%" :: _) = "" (* error *)
   | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
 
 val encode_str = String.translate meta_char
+val decode_str = String.explode #> unmeta_chars []
+
 val encode_strs = map encode_str #> space_implode " "
-val unencode_str = String.explode #> unmeta_chars []
-val unencode_strs =
-  space_explode " " #> filter_out (curry (op =) "") #> map unencode_str
+val decode_strs = space_explode " " #> filter_out (curry (op =) "") #> map decode_str
 
 (* Avoid scientific notation *)
 fun safe_str_of_real r =
   if r < 0.00001 then "0.00001"
   else if r >= 1000000.0 then "1000000"
   else Markup.print_real r
 
-val encode_plain_feature = space_implode "|" o map encode_str
+val encode_unweighted_feature = map encode_str #> space_implode "|"
+val decode_unweighted_feature = space_explode "|" #> map decode_str
 
 fun encode_feature (names, weight) =
-  encode_plain_feature names ^ (if Real.== (weight, 1.0) then "" else "=" ^ safe_str_of_real weight)
-
-val encode_plain_features = map encode_plain_feature #> space_implode " "
+  encode_unweighted_feature names ^ (if Real.== (weight, 1.0) then "" else "=" ^ safe_str_of_real weight)
+
+val encode_unweighted_features = map encode_unweighted_feature #> space_implode " "
+val decode_unweighted_features = space_explode " " #> map decode_unweighted_feature
+
 val encode_features = map encode_feature #> space_implode " "
 
-fun str_of_learn (name, parents, feats : string list list, deps) =
+fun str_of_learn (name, parents, feats, deps) =
   "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
-  encode_plain_features feats ^ "; " ^ encode_strs deps ^ "\n"
-
-fun str_of_relearn (name, deps) =
-  "p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n"
+  encode_unweighted_features feats ^ "; " ^ encode_strs deps ^ "\n"
+
+fun str_of_relearn (name, deps) = "p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n"
 
 fun str_of_query max_suggs (learns, hints, parents, feats) =
   implode (map str_of_learn learns) ^
-  "? " ^ string_of_int max_suggs ^ " # " ^ encode_strs parents ^ "; " ^
-  encode_features feats ^
+  "? " ^ string_of_int max_suggs ^ " # " ^ encode_strs parents ^ "; " ^ encode_features feats ^
   (if null hints then "" else "; " ^ encode_strs hints) ^ "\n"
 
-(* The suggested weights don't make much sense. *)
+(* The suggested weights do not make much sense. *)
 fun extract_suggestion sugg =
   (case space_explode "=" sugg of
-    [name, _ (* weight *)] =>
-    SOME (unencode_str name (* , Real.fromString weight |> the_default 1.0 *))
-  | [name] => SOME (unencode_str name (* , 1.0 *))
+    [name, _ (* weight *)] => SOME (decode_str name)
+  | [name] => SOME (decode_str name)
   | _ => NONE)
 
 fun extract_suggestions line =
   (case space_explode ":" line of
-    [goal, suggs] => (unencode_str goal, map_filter extract_suggestion (space_explode " " suggs))
+    [goal, suggs] => (decode_str goal, map_filter extract_suggestion (space_explode " " suggs))
   | _ => ("", []))
 
 structure MaSh =
 struct
 

 end;
 
 
 (*** Middle-level communication with MaSh ***)
 
-datatype proof_kind =
-  Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop
+datatype proof_kind = Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop
 
 fun str_of_proof_kind Isar_Proof = "i"
   | str_of_proof_kind Automatic_Proof = "a"
   | str_of_proof_kind Isar_Proof_wegen_Prover_Flop = "x"
 
-fun proof_kind_of_str "i" = Isar_Proof
-  | proof_kind_of_str "a" = Automatic_Proof
+fun proof_kind_of_str "a" = Automatic_Proof
   | proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop
-
-(* FIXME: Here a "Graph.update_node" function would be useful *)
-fun update_access_graph_node (name, kind) =
-  Graph.default_node (name, Isar_Proof)
-  #> kind <> Isar_Proof ? Graph.map_node name (K kind)
+  | proof_kind_of_str _ (* "i" *) = Isar_Proof
 
 fun try_graph ctxt when def f =
   f ()
-  handle Graph.CYCLES (cycle :: _) =>
-         (trace_msg ctxt (fn () =>
-              "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
-       | Graph.DUP name =>
-         (trace_msg ctxt (fn () =>
-              "Duplicate fact " ^ quote name ^ " when " ^ when); def)
-       | Graph.UNDEF name =>
-         (trace_msg ctxt (fn () =>
-              "Unknown fact " ^ quote name ^ " when " ^ when); def)
-       | exn =>
-         if Exn.is_interrupt exn then
-           reraise exn
-         else
-           (trace_msg ctxt (fn () =>
-                "Internal error when " ^ when ^ ":\n" ^
-                Runtime.exn_message exn); def)
+  handle
+    Graph.CYCLES (cycle :: _) =>
+    (trace_msg ctxt (fn () => "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
+  | Graph.DUP name =>
+    (trace_msg ctxt (fn () => "Duplicate fact " ^ quote name ^ " when " ^ when); def)
+  | Graph.UNDEF name =>
+    (trace_msg ctxt (fn () => "Unknown fact " ^ quote name ^ " when " ^ when); def)
+  | exn =>
+    if Exn.is_interrupt exn then
+      reraise exn
+    else
+      (trace_msg ctxt (fn () => "Internal error when " ^ when ^ ":\n" ^ Runtime.exn_message exn);
+       def)
 
 fun graph_info G =
   string_of_int (length (Graph.keys G)) ^ " node(s), " ^
   string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^
   " edge(s), " ^
   string_of_int (length (Graph.minimals G)) ^ " minimal, " ^
   string_of_int (length (Graph.maximals G)) ^ " maximal"
 
 type mash_state =
-  {access_G : unit Graph.T,
+  {access_G : (proof_kind * string list 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 []}
+val empty_state = {access_G = Graph.empty, num_known_facts = 0, dirty = SOME []} : mash_state
 
 local
 
-val version = "*** MaSh version 20131206 ***"
+val version = "*** MaSh version 20140516 ***"
 
 exception FILE_VERSION_TOO_NEW of unit
 
 fun extract_node line =
   (case space_explode ":" line of
-    [head, parents] =>
-    (case space_explode " " head of
-      [kind, name] =>
-      SOME (unencode_str name, unencode_strs parents,
-        try proof_kind_of_str kind |> the_default Isar_Proof)
+    [head, tail] =>
+    (case (space_explode " " head, map (unprefix " ") (space_explode ";" tail)) of
+      ([kind, name], [parents, feats, deps]) =>
+      SOME (proof_kind_of_str kind, decode_str name, decode_strs parents,
+        decode_unweighted_features feats, decode_strs deps)
     | _ => NONE)
   | _ => NONE)
 
 fun load_state _ _ (state as (true, _)) = state
   | load_state ctxt overlord _ =

       (true,
        (case try File.read_lines path of
          SOME (version' :: node_lines) =>
          let
            fun add_edge_to name parent =
-             Graph.default_node (parent, Isar_Proof)
+             Graph.default_node (parent, (Isar_Proof, [], []))
              #> Graph.add_edge (parent, name)
            fun add_node line =
              (case extract_node line of
-               NONE => I (* shouldn't happen *)
-             | SOME (name, parents, kind) =>
-               update_access_graph_node (name, kind) #> fold (add_edge_to name) parents)
+               NONE => I (* should not happen *)
+             | SOME (kind, name, parents, feats, deps) =>
+               Graph.default_node (name, (kind, feats, deps))
+               #> Graph.map_node name (K (kind, feats, deps))
+               #> fold (add_edge_to name) parents)
            val (access_G, num_known_facts) =
              (case string_ord (version', version) of
                EQUAL =>
                (try_graph ctxt "loading state" Graph.empty (fn () =>
                   fold add_node node_lines Graph.empty),
                 length node_lines)
-             | LESS =>
-               (* can't parse old file *)
-               (MaSh.unlearn ctxt overlord; (Graph.empty, 0))
+             | LESS => (MaSh.unlearn ctxt overlord; (Graph.empty, 0)) (* cannot parse old file *)
              | 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 []}
+           trace_msg ctxt (fn () => "Loaded fact graph (" ^ graph_info access_G ^ ")");
+           {access_G = access_G, num_known_facts = num_known_facts, dirty = 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_unweighted_features feats ^ "; " ^ encode_strs deps ^ "\n"
+
 fun save_state _ (state as {dirty = SOME [], ...}) = state
   | save_state ctxt {access_G, num_known_facts, dirty} =
     let
-      fun str_of_entry (name, parents, kind) =
-        str_of_proof_kind kind ^ " " ^ encode_str name ^ ": " ^
-        encode_strs parents ^ "\n"
-      fun append_entry (name, (kind, (parents, _))) =
-        cons (name, Graph.Keys.dest parents, kind)
+      fun append_entry (name, ((kind, feats, deps), (parents, _))) =
+        cons (kind, name, Graph.Keys.dest parents, feats, deps)
+
       val (banner, entries) =
         (case dirty 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) (mash_state_file ());
       trace_msg ctxt (fn () =>
-          "Saved fact graph (" ^ graph_info access_G ^
-          (case dirty of
-             SOME dirty =>
-             "; " ^ string_of_int (length dirty) ^ " dirty fact(s)"
-           | _ => "") ^  ")");
+        "Saved fact graph (" ^ graph_info access_G ^
+        (case dirty of
+          SOME dirty => "; " ^ string_of_int (length dirty) ^ " dirty fact(s)"
+        | _ => "") ^  ")");
       {access_G = access_G, num_known_facts = num_known_facts, dirty = SOME []}
     end
 
 val global_state =
   Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state)
 
 in
 
 fun map_state ctxt overlord f =
-  Synchronized.change global_state
-                      (load_state ctxt overlord ##> (f #> save_state ctxt))
+  Synchronized.change global_state (load_state ctxt overlord ##> (f #> save_state ctxt))
   handle FILE_VERSION_TOO_NEW () => ()
 
 fun peek_state ctxt overlord f =
-  Synchronized.change_result global_state
-      (perhaps (try (load_state ctxt overlord)) #> `snd #>> f)
+  Synchronized.change_result global_state (perhaps (try (load_state ctxt overlord)) #> `snd #>> f)
 
 fun clear_state ctxt overlord =
-  Synchronized.change global_state (fn _ =>
-      (MaSh.unlearn ctxt overlord; (* also removes the state file *)
-       (false, empty_state)))
+  (* "unlearn" also removes the state file *)
+  Synchronized.change global_state (fn _ => (MaSh.unlearn ctxt overlord; (false, empty_state)))
 
 end
 
 fun mash_unlearn ctxt ({overlord, ...} : params) =
   (clear_state ctxt overlord; Output.urgent_message "Reset MaSh.")

     term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth in_goal ts
     |> scope <> Global ? cons local_feature
   end
 
 (* Too many dependencies is a sign that a decision procedure is at work. There
-   isn't much to learn from such proofs. *)
+   is not much to learn from such proofs. *)
 val max_dependencies = 20
 
 val prover_default_max_facts = 25
 
 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *)

         if exists (is_dep dep) accum then
           accum
         else
           (case find_first (is_dep dep) facts of
             SOME ((_, status), th) => accum @ [(("", status), th)]
-          | NONE => accum (* shouldn't happen *))
+          | NONE => accum (* should not happen *))
       val mepo_facts =
         facts
         |> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE
              hyp_ts concl_t
       val facts =

           else
             let
               val parents = maximal_wrt_access_graph access_G facts
               val goal_feats =
                 features_of ctxt thy num_facts const_tab (Local, General) true (concl_t :: hyp_ts)
-              val chained_feats =
-                chained
+              val chained_feats = chained
                 |> map (rpair 1.0)
                 |> map (chained_or_extra_features_of chained_feature_factor)
                 |> rpair [] |-> fold (union (eq_fst (op =)))
-              val extra_feats =
-                facts
+              val extra_feats = facts
                 |> take (Int.max (0, num_extra_feature_facts - length chained))
                 |> filter fact_has_right_theory
                 |> weight_facts_steeply
                 |> map (chained_or_extra_features_of extra_feature_factor)
                 |> rpair [] |-> fold (union (eq_fst (op =)))
               val feats =
-                fold (union (eq_fst (op =))) [chained_feats, extra_feats]
-                     goal_feats
+                fold (union (eq_fst (op =))) [chained_feats, extra_feats] goal_feats
                 |> debug ? sort (Real.compare o swap o pairself snd)
-              val hints =
-                chained |> filter (is_fact_in_graph access_G o snd)
-                        |> map (nickname_of_thm o snd)
+              val hints = chained
+                |> filter (is_fact_in_graph access_G o snd)
+                |> map (nickname_of_thm o snd)
             in
-              (access_G, MaSh.query ctxt overlord max_facts
-                                    ([], hints, parents, feats))
+              (access_G, MaSh.query ctxt overlord max_facts ([], hints, parents, feats))
             end)
-    val unknown = facts |> filter_out (is_fact_in_graph access_G o snd)
+    val unknown = filter_out (is_fact_in_graph access_G o snd) facts
   in
     find_mash_suggestions ctxt max_facts suggs facts chained unknown
     |> pairself (map fact_of_raw_fact)
   end
 
 fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (learns, graph) =
   let
     fun maybe_learn_from from (accum as (parents, graph)) =
       try_graph ctxt "updating graph" accum (fn () =>
-          (from :: parents, Graph.add_edge_acyclic (from, name) graph))
-    val graph = graph |> Graph.default_node (name, Isar_Proof)
+        (from :: parents, Graph.add_edge_acyclic (from, name) graph))
+    val graph = graph |> Graph.default_node (name, (Isar_Proof, feats, deps))
     val (parents, graph) = ([], graph) |> fold maybe_learn_from parents
     val (deps, _) = ([], graph) |> fold maybe_learn_from deps
   in ((name, parents, feats, deps) :: learns, graph) end
 
 fun relearn_wrt_access_graph ctxt (name, deps) (relearns, graph) =
   let
     fun maybe_relearn_from from (accum as (parents, graph)) =
       try_graph ctxt "updating graph" accum (fn () =>
-          (from :: parents, Graph.add_edge_acyclic (from, name) graph))
-    val graph = graph |> update_access_graph_node (name, Automatic_Proof)
+        (from :: parents, Graph.add_edge_acyclic (from, name) graph))
+    val graph = graph |> Graph.map_node name (fn (_, feats, _) => (Automatic_Proof, feats, deps))
     val (deps, _) = ([], graph) |> fold maybe_relearn_from deps
   in ((name, deps) :: relearns, graph) end
 
 fun flop_wrt_access_graph name =
-  update_access_graph_node (name, Isar_Proof_wegen_Prover_Flop)
+  Graph.map_node name (fn (_, feats, deps) => (Isar_Proof_wegen_Prover_Flop, feats, deps))
 
 val learn_timeout_slack = 2.0
 
 fun launch_thread timeout task =
   let

 fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover save auto_level
     run_prover learn_timeout facts =
   let
     val timer = Timer.startRealTimer ()
     fun next_commit_time () = Time.+ (Timer.checkRealTimer timer, commit_timeout)
+
     val {access_G, ...} = peek_state ctxt overlord I
     val is_in_access_G = is_fact_in_graph access_G o snd
     val no_new_facts = forall is_in_access_G facts
   in
     if no_new_facts andalso not run_prover then
       if auto_level < 2 then
-        "No new " ^ (if run_prover then "automatic" else "Isar") ^
-        " proofs to learn." ^
+        "No new " ^ (if run_prover then "automatic" else "Isar") ^ " proofs to learn." ^
         (if auto_level = 0 andalso not run_prover then
-           "\n\nHint: Try " ^ sendback learn_proverN ^
-           " to learn from an automatic prover."
+           "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover."
          else
            "")
       else
         ""
     else
       let
         val name_tabs = build_name_tables nickname_of_thm facts
+
         fun deps_of status th =
           if no_dependencies_for_status status then
             SOME []
           else if run_prover then
-            prover_dependencies_of ctxt params prover auto_level facts name_tabs
-                                   th
-            |> (fn (false, _) => NONE
-                 | (true, deps) => trim_dependencies deps)
+            prover_dependencies_of ctxt params prover auto_level facts name_tabs th
+            |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps)
           else
             isar_dependencies_of name_tabs th
             |> trim_dependencies
+
         fun do_commit [] [] [] state = state
           | do_commit learns relearns flops {access_G, num_known_facts, dirty} =
             let
               val was_empty = Graph.is_empty access_G
-              val (learns, access_G) =
-                ([], access_G) |> fold (learn_wrt_access_graph ctxt) learns
+              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 =

                   (false, SOME names, []) => SOME (map #1 learns @ names)
                 | _ => NONE)
             in
               MaSh.learn ctxt overlord (save andalso null relearns) (rev learns);
               MaSh.relearn ctxt overlord save relearns;
-              {access_G = access_G, num_known_facts = num_known_facts,
-               dirty = dirty}
+              {access_G = access_G, num_known_facts = num_known_facts, dirty = dirty}
             end
+
         fun commit last learns relearns flops =
           (if debug andalso auto_level = 0 then
              Output.urgent_message "Committing..."
            else
              ();

                string_of_time commit_timeout ^ "."
                |> Output.urgent_message
              end
            else
              ())
+
         fun learn_new_fact _ (accum as (_, (_, _, true))) = accum
           | learn_new_fact (parents, ((_, stature as (_, status)), th))
-                           (learns, (n, next_commit, _)) =
+              (learns, (n, next_commit, _)) =
             let
               val name = nickname_of_thm th
               val feats =
                 features_of ctxt (theory_of_thm th) 0 Symtab.empty stature false [prop_of th]
                 |> map fst

                 if Time.> (Timer.checkRealTimer timer, next_commit) then
                   (commit false learns [] []; ([], next_commit_time ()))
                 else
                   (learns, next_commit)
               val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
-            in (learns, (n, next_commit, timed_out)) end
+            in
+              (learns, (n, next_commit, timed_out))
+            end
+
         val n =
           if no_new_facts then
             0
           else
             let
-              val new_facts =
-                facts |> sort (crude_thm_ord o pairself snd)
-                      |> attach_parents_to_facts []
-                      |> filter_out (is_in_access_G o snd)
+              val new_facts = facts
+                |> sort (crude_thm_ord o pairself snd)
+                |> attach_parents_to_facts []
+                |> filter_out (is_in_access_G o snd)
               val (learns, (n, _, _)) =
                 ([], (0, next_commit_time (), false))
                 |> fold learn_new_fact new_facts
-            in commit true learns [] []; n end
+            in
+              commit true learns [] []; n
+            end
+
         fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
-          | relearn_old_fact ((_, (_, status)), th)
-                             ((relearns, flops), (n, next_commit, _)) =
+          | relearn_old_fact ((_, (_, status)), th) ((relearns, flops), (n, next_commit, _)) =
             let
               val name = nickname_of_thm th
               val (n, relearns, flops) =
                 (case deps_of status th of
                   SOME deps => (n + 1, (name, deps) :: relearns, flops)
                 | NONE => (n, relearns, name :: flops))
               val (relearns, flops, next_commit) =
                 if Time.> (Timer.checkRealTimer timer, next_commit) then
-                  (commit false [] relearns flops;
-                   ([], [], next_commit_time ()))
+                  (commit false [] relearns flops; ([], [], next_commit_time ()))
                 else
                   (relearns, flops, next_commit)
               val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
-            in ((relearns, flops), (n, next_commit, timed_out)) end
+            in
+              ((relearns, flops), (n, next_commit, timed_out))
+            end
+
         val n =
           if not run_prover then
             n
           else
             let
               val max_isar = 1000 * max_dependencies
-              fun kind_of_proof th =
-                try (Graph.get_node access_G) (nickname_of_thm th)
-                |> the_default Isar_Proof
-              fun priority_of (_, th) =
+
+              val kind_of_proof =
+                nickname_of_thm #> try (#1 o Graph.get_node access_G) #> the_default Isar_Proof
+
+              fun priority_of th =
                 random_range 0 max_isar
                 + (case kind_of_proof th of
                      Isar_Proof => 0
                    | Automatic_Proof => 2 * max_isar
                    | Isar_Proof_wegen_Prover_Flop => max_isar)
                 - 100 * length (isar_dependencies_of name_tabs th)
-              val old_facts =
-                facts |> filter is_in_access_G
-                      |> map (`priority_of)
-                      |> sort (int_ord o pairself fst)
-                      |> map snd
+
+              val old_facts = facts
+                |> filter is_in_access_G
+                |> map (`(priority_of o snd))
+                |> sort (int_ord o pairself fst)
+                |> map snd
               val ((relearns, flops), (n, _, _)) =
                 (([], []), (n, next_commit_time (), false))
                 |> fold relearn_old_fact old_facts
-            in commit true [] relearns flops; n end
+            in
+              commit true [] relearns flops; n
+            end
       in
         if verbose orelse auto_level < 2 then
           "Learned " ^ string_of_int n ^ " nontrivial " ^
           (if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s n ^
           (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer)

 val mepo_weight = 0.5
 val mash_weight = 0.5
 
 val max_facts_to_learn_before_query = 100
 
-(* The threshold should be large enough so that MaSh doesn't kick in for Auto
-   Sledgehammer and Try. *)
+(* The threshold should be large enough so that MaSh does not get activated for Auto Sledgehammer
+   and Try. *)
 val min_secs_for_learning = 15
 
 fun relevant_facts ctxt (params as {overlord, blocking, learn, fact_filter, timeout, ...}) prover
     max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
   if not (subset (op =) (the_list fact_filter, fact_filters)) then

       | _ => [(effective_fact_filter, mesh)])
     end
 
 fun kill_learners ctxt ({overlord, ...} : params) =
   (Async_Manager.kill_threads MaShN "learner"; MaSh.shutdown ctxt overlord)
+
 fun running_learners () = Async_Manager.running_threads MaShN "learner"
 
 end;