src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

       | add_classes S =
         fold (`(Sorts.super_classes classes)
               #> swap #> op ::
               #> subtract (op =) @{sort type} #> map massage_long_name
               #> map class_feature_of
-              #> union (op = o pairself fst)) S
+              #> union (eq_fst (op =))) S
 
     fun pattify_type 0 _ = []
       | pattify_type _ (Type (s, [])) =
         if member (op =) bad_types s then [] else [massage_long_name s]
       | pattify_type depth (Type (s, U :: Ts)) =

       | pattify_type _ (TFree (_, S)) =
         maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
       | pattify_type _ (TVar (_, S)) =
         maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
     fun add_type_pat depth T =
-      union (op = o pairself fst) (map type_feature_of (pattify_type depth T))
+      union (eq_fst (op =)) (map type_feature_of (pattify_type depth T))
     fun add_type_pats 0 _ = I
       | add_type_pats depth t =
         add_type_pat depth t #> add_type_pats (depth - 1) t
     fun add_type T =
       add_type_pats type_max_depth T

           map_product (fn ppw as (p, pw) =>
               fn ("", _) => ppw
                | (q, qw) => (p ^ "(" ^ q ^ ")", pw + qw)) ps qs
         end
       | pattify_term _ _ _ _ = []
-    fun add_term_pat Ts depth =
-      union (op = o pairself fst) o pattify_term Ts [] depth
+    fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts []
     fun add_term_pats _ 0 _ = I
       | add_term_pats Ts depth t =
         add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t
     fun add_term Ts = add_term_pats Ts term_max_depth
     fun add_subterms Ts t =

 
 fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm
 
 val chained_feature_factor = 0.5
 val extra_feature_factor = 0.1
-val num_extra_feature_facts = 0 (* FUDGE *)
+val num_extra_feature_facts = 10 (* FUDGE *)
 
 (* FUDGE *)
 fun weight_of_proximity_fact rank =
   Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0
 

 val max_proximity_facts = 100
 
 fun find_mash_suggestions _ _ [] _ _ raw_unknown = ([], raw_unknown)
   | find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown =
     let
-      val inter_fact = inter (Thm.eq_thm_prop o pairself snd)
+      val inter_fact = inter (eq_snd Thm.eq_thm_prop)
       val raw_mash = find_suggested_facts ctxt facts suggs
       val proximate = take max_proximity_facts facts
       val unknown_chained = inter_fact raw_unknown chained
       val unknown_proximate = inter_fact raw_unknown proximate
       val mess =
         [(0.9 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])),
          (0.4 (* FUDGE *), (weight_facts_smoothly unknown_proximate, [])),
          (0.1 (* FUDGE *), (weight_facts_steeply raw_mash, raw_unknown))]
       val unknown =
         raw_unknown
-        |> fold (subtract (Thm.eq_thm_prop o pairself snd))
+        |> fold (subtract (eq_snd Thm.eq_thm_prop))
                 [unknown_chained, unknown_proximate]
-    in (mesh_facts (Thm.eq_thm_prop o pairself snd) max_facts mess, unknown) end
+    in (mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess, unknown) end
 
 fun add_const_counts t =
   fold (fn s => Symtab.map_default (s, 0) (Integer.add 1))
        (Term.add_const_names t [])
 

                             (Local, General) (concl_t :: hyp_ts)
               val chained_feats =
                 chained
                 |> map (rpair 1.0)
                 |> map (chained_or_extra_features_of chained_feature_factor)
-                |> rpair [] |-> fold (union (op = o pairself fst))
+                |> rpair [] |-> fold (union (eq_fst (op =)))
               val extra_feats =
                 facts
                 |> take (Int.max (0, num_extra_feature_facts - length chained))
                 |> weight_facts_steeply
                 |> map (chained_or_extra_features_of extra_feature_factor)
-                |> rpair [] |-> fold (union (op = o pairself fst))
+                |> rpair [] |-> fold (union (eq_fst (op =)))
               val feats =
-                fold (union (op = o pairself fst)) [chained_feats, extra_feats]
+                fold (union (eq_fst (op =))) [chained_feats, extra_feats]
                      goal_feats
               val hints =
                 chained |> filter (is_fact_in_graph access_G o snd)
                         |> map (nickname_of_thm o snd)
             in

            |> (if effective_fact_filter <> mashN then
                  cons (mepo_weight, (mepo (), []))
                else
                  I)
       val mesh =
-        mesh_facts (Thm.eq_thm_prop o pairself snd) max_facts mess
+        mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess
         |> add_and_take
     in
       if save then MaSh.save ctxt overlord else ();
       case (fact_filter, mess) of
         (NONE, [(_, (mepo, _)), (_, (mash, _))]) =>