# HG changeset patch
# User wenzelm
# Date 1583751148 -3600
# Node ID abe723ff3f7fe1ea9ba43795bb354a821e3d3b24
# Parent  d7b0d078266d1c7ecfc23becf354ad6c87fc4467
tuned signature;

diff -r d7b0d078266d -r abe723ff3f7f src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sat Mar 07 12:19:41 2020 +0100
+++ b/src/Pure/sorts.ML	Mon Mar 09 11:52:28 2020 +0100
@@ -134,13 +134,13 @@
 
 (* class relations *)
 
-val class_less = Graph.is_edge o classes_of;
+val class_less : algebra -> class * class -> bool = Graph.is_edge o classes_of;
 fun class_le algebra (c1, c2) = c1 = c2 orelse class_less algebra (c1, c2);
 
 
 (* sort relations *)
 
-fun sort_le algebra (S1, S2) =
+fun sort_le algebra (S1: sort, S2: sort) =
   S1 = S2 orelse forall (fn c2 => exists (fn c1 => class_le algebra (c1, c2)) S1) S2;
 
 fun sorts_le algebra (Ss1, Ss2) =
@@ -454,7 +454,7 @@
 
 (* witness_sorts *)
 
-fun witness_sorts algebra types hyps sorts =
+fun witness_sorts algebra ground_types hyps sorts =
   let
     fun le S1 S2 = sort_le algebra (S1, S2);
     fun get S2 (T, S1) = if le S1 S2 then SOME (T, S2) else NONE;
@@ -469,7 +469,7 @@
             | NONE =>
                 (case get_first (get S) hyps of
                   SOME w => (SOME w, (w :: solved, failed))
-                | NONE => witn_types path types S (solved, failed)))
+                | NONE => witn_types path ground_types S (solved, failed)))
 
     and witn_sorts path x = fold_map (witn_sort path) x