# HG changeset patch
# User wenzelm
# Date 847280971 -3600
# Node ID 4d43e7486164b7a38bba4c0d8de9348c24cfd3d0
# Parent  f53171d7f86ca65749ce9c51d0c4a4338984b3c4
tuned fix_shyps a little bit more;

diff -r f53171d7f86c -r 4d43e7486164 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Nov 05 18:35:40 1996 +0100
+++ b/src/Pure/thm.ML	Wed Nov 06 12:49:31 1996 +0100
@@ -415,12 +415,17 @@
 
 (* basic utils *)
 
-(*accumulate sorts suppressing duplicates; these are coded low level
+(*accumulate sorts suppressing duplicates; these are coded low levelly
   to improve efficiency a bit*)
 
+fun mem_sort (_:sort) [] = false
+  | mem_sort S (S' :: Ss) = S = S' orelse mem_sort S Ss;
+
+fun ins_sort S Ss = if mem_sort S Ss then Ss else S :: Ss;
+
 fun add_typ_sorts (Type (_, Ts), Ss) = add_typs_sorts (Ts, Ss)
-  | add_typ_sorts (TFree (_, S), Ss) = S ins Ss
-  | add_typ_sorts (TVar (_, S), Ss) = S ins Ss
+  | add_typ_sorts (TFree (_, S), Ss) = ins_sort S Ss
+  | add_typ_sorts (TVar (_, S), Ss) = ins_sort S Ss
 and add_typs_sorts ([], Ss) = Ss
   | add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss));