src/HOL/Tools/Nitpick/nitpick_preproc.ML

          | _ => false) ? cons args
     fun call_sets [] [] vs = [vs]
       | call_sets [] uss vs = vs :: call_sets uss [] []
       | call_sets ([] :: _) _ _ = []
       | call_sets ((t :: ts) :: tss) uss vs =
-        OrdList.insert Term_Ord.term_ord t vs |> call_sets tss (ts :: uss)
+        Ord_List.insert Term_Ord.term_ord t vs |> call_sets tss (ts :: uss)
     val sets = call_sets (fun_calls t [] []) [] []
     val indexed_sets = sets ~~ (index_seq 0 (length sets))
   in
     fold_rev (fn (set, j) =>
                  case set of

                  | [t as Free _] => cons (j, SOME t)
                  | _ => I) indexed_sets []
   end
 fun static_args_in_terms hol_ctxt x =
   map (static_args_in_term hol_ctxt x)
-  #> fold1 (OrdList.inter (prod_ord int_ord (option_ord Term_Ord.term_ord)))
+  #> fold1 (Ord_List.inter (prod_ord int_ord (option_ord Term_Ord.term_ord)))
 
 fun overlapping_indices [] _ = []
   | overlapping_indices _ [] = []
   | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
     if j1 < j2 then overlapping_indices ps1' ps2

       |> map (fn (x, zs) =>
                  (x, zs |> member (op =) ts (Const x) ? cons ([], [], x)))
     fun generality (js, _, _) = ~(length js)
     fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
       x1 <> x2 andalso length j2 < length j1 andalso
-      OrdList.subset (prod_ord int_ord Term_Ord.term_ord) (j2 ~~ t2, j1 ~~ t1)
+      Ord_List.subset (prod_ord int_ord Term_Ord.term_ord) (j2 ~~ t2, j1 ~~ t1)
     fun do_pass_1 _ [] [_] [_] = I
       | do_pass_1 T skipped _ [] = do_pass_2 T skipped
       | do_pass_1 T skipped all (z :: zs) =
         case filter (is_more_specific z) all
              |> sort (int_ord o pairself generality) of