# HG changeset patch
# User wenzelm
# Date 1564841434 -7200
# Node ID 185c63c40ad744321182f3a0a3d5e1bd0e67d0c7
# Parent  9ac6426ab8e055ec06838a40b02255bc8112cc14
more complete completions according to Sorts.insert_complete_ars (cf. 13199740ced6), e.g. relevant for theories HOL-ex.Word_Type, HOL-Matrix_LP.SparseMatrix;

diff -r 9ac6426ab8e0 -r 185c63c40ad7 src/Pure/thm.ML
--- 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 =