more complete completions according to Sorts.insert_complete_ars (cf. 13199740ced6), e.g. relevant for theories HOL-ex.Word_Type, HOL-Matrix_LP.SparseMatrix;

--- a/src/Pure/thm.ML	Sat Aug 03 15:48:28 2019 +0200
+++ b/src/Pure/thm.ML	Sat Aug 03 16:10:34 2019 +0200
@@ -2207,12 +2207,10 @@
 
 fun insert_arity_completions thy t ((c, Ss), ((th, thy_name))) (finished, arities) =
   let
-    val algebra = Sign.classes_of thy;
     val ars = Symtab.lookup_list arities t;
     val completions =
       Sign.super_classes thy c |> map_filter (fn c1 =>
-        if exists (fn ((c', Ss'), _) => c1 = c' andalso Sorts.sorts_le algebra (Ss', Ss)) ars
-        then NONE
+        if exists (fn ((c', Ss'), _) => c1 = c' andalso Ss' = Ss) ars then NONE
         else
           let
             val th1 =