Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned fix_shyps a little bit more;
authorwenzelm
Wed, 06 Nov 1996 12:49:31 +0100
changeset 2163 4d43e7486164
parent 2162 f53171d7f86c
child 2164 c87368fc736b
tuned fix_shyps a little bit more;
src/Pure/thm.ML file | annotate | diff | comparison | revisions 
--- 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));
isabelle