src/HOL/Tools/Nitpick/nitpick_model.ML

   nat_subscript (j + 1)
   |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
      ? prefix "\<^isub>,"
 (* string -> typ -> int -> string *)
 fun atom_name prefix (T as Type (s, _)) j =
-    prefix ^ substring (short_name s, 0, 1) ^ atom_suffix s j
+    prefix ^ substring (shortest_name s, 0, 1) ^ atom_suffix s j
   | atom_name prefix (T as TFree (s, _)) j =
     prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j
   | atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
 (* bool -> typ -> int -> term *)
 fun atom for_auto T j =

       | aux T1 T2 ((t1, t2) :: ps) =
         Const (@{const_name fun_upd}, [T1 --> T2, T1, T2] ---> T1 --> T2)
         $ aux T1 T2 ps $ t1 $ t2
   in aux T1 T2 o rev end
 (* term -> bool *)
-fun is_plain_fun (Const (s, _)) = s mem [@{const_name undefined}, non_opt_name]
+fun is_plain_fun (Const (s, _)) =
+    (s = @{const_name undefined} orelse s = non_opt_name)
   | is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) =
     is_plain_fun t0
   | is_plain_fun _ = false
 (* term -> bool * (term list * term list) *)
 val dest_plain_fun =

             val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
                                  constrs
             val real_j = j + offset_of_type ofs T
             val constr_x as (constr_s, constr_T) =
               get_first (fn (jss, {const, ...}) =>
-                            if [real_j] mem jss then SOME const else NONE)
+                            if member (op =) jss [real_j] then SOME const
+                            else NONE)
                         (discr_jsss ~~ constrs) |> the
             val arg_Ts = curried_binder_types constr_T
             val sel_xs = map (boxed_nth_sel_for_constr ext_ctxt constr_x)
                              (index_seq 0 (length arg_Ts))
             val sel_Rs =

             val arg_jsss =
               map (map_filter (fn js => if hd js = real_j then SOME (tl js)
                                         else NONE)) sel_jsss
             val uncur_arg_Ts = binder_types constr_T
           in
-            if co andalso (T, j) mem seen then
+            if co andalso member (op =) seen (T, j) then
               Var (var ())
             else
               let
                 val seen = seen |> co ? cons (T, j)
                 val ts =

                   else
                     list_comb (Const constr_x, ts)
               in
                 if co then
                   let val var = var () in
-                    if exists_subterm (equal (Var var)) t then
+                    if exists_subterm (curry (op =) (Var var)) t then
                       Const (@{const_name The}, (T --> bool_T) --> T)
                       $ Abs ("\<omega>", T,
                              Const (@{const_name "op ="}, [T, T] ---> bool_T)
                              $ Bound 0 $ abstract_over (Var var, t))
                     else

         let
           val jss1 = all_combinations_for_rep R1
           val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
           val ts2 =
             map (fn js => term_for_rep seen T2 T2 (Atom (2, 0))
-                                       [[int_for_bool (js mem jss)]]) jss1
+                                       [[int_for_bool (member (op =) jss js)]])
+                jss1
         in make_fun false T1 T2 T' ts1 ts2 end
       | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss =
         let
           val arity1 = arity_of_rep R1
           val jss1 = all_combinations_for_rep R1

     let val T = fastype_of t1 in
       if exists_subtype (member (op =) coTs) T then
         let
           val ((head1, args1), (head2, args2)) =
             pairself (strip_comb o unfold_outer_the_binders) (t1, t2)
-          val max_depth = max_depth - (if T mem coTs then 1 else 0)
+          val max_depth = max_depth - (if member (op =) coTs T then 1 else 0)
         in
           head1 = head2
           andalso forall (bisimilar_values coTs max_depth) (args1 ~~ args2)
         end
       else

     val (skolem_names, nonskolem_nonsel_names) =
       List.partition is_skolem_name nonsel_names
     val (eval_names, noneval_nonskolem_nonsel_names) =
       List.partition (String.isPrefix eval_prefix o nickname_of)
                      nonskolem_nonsel_names
-      ||> filter_out (equal @{const_name bisim_iterator_max} o nickname_of)
+      ||> filter_out (curry (op =) @{const_name bisim_iterator_max}
+                      o nickname_of)
     val free_names =
       map (fn x as (s, T) =>
-              case filter (equal x o pairf nickname_of (unbox_type o type_of))
+              case filter (curry (op =) x
+                           o pairf nickname_of (unbox_type o type_of))
                           free_names of
                 [name] => name
               | [] => FreeName (s, T, Any)
               | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model",
                                  [Const x])) all_frees