Removal of polymorphic equality via mem, subset, eq_set, etc

--- a/src/Pure/display.ML	Tue Nov 12 13:20:36 1996 +0100
+++ b/src/Pure/display.ML	Wed Nov 13 10:38:08 1996 +0100
@@ -118,7 +118,7 @@
 
   fun ins_entry (x, y) [] = [(x, [y])]
     | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
-        if x = x' then (x', y ins ys') :: pairs
+        if x = x' then (x', y ins_string ys') :: pairs
         else pair :: ins_entry (x, y) pairs;
 
   fun add_type_env (Free (x, T), env) = ins_entry (T, x) env

--- a/src/Pure/drule.ML	Tue Nov 12 13:20:36 1996 +0100
+++ b/src/Pure/drule.ML	Wed Nov 13 10:38:08 1996 +0100
@@ -461,7 +461,7 @@
     let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
         and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
     in  Sign.eq_sg (sg1,sg2) andalso
-        eq_set (shyps1, shyps2) andalso
+        eq_set_sort (shyps1, shyps2) andalso
         aconvs(hyps1,hyps2) andalso
         prop1 aconv prop2
     end;
@@ -473,7 +473,7 @@
     let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
         and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
     in  Sign.same_sg (sg1,sg2) andalso
-        eq_set (shyps1, shyps2) andalso
+        eq_set_sort (shyps1, shyps2) andalso
         aconvs(hyps1,hyps2) andalso
         prop1 aconv prop2
     end;

--- a/src/Pure/sign.ML	Tue Nov 12 13:20:36 1996 +0100
+++ b/src/Pure/sign.ML	Wed Nov 13 10:38:08 1996 +0100
@@ -88,20 +88,30 @@
 val tsig_of = #tsig o rep_sg;
 
 
-(* stamps *)
+(*** Stamps ***)
+
+(*Avoiding polymorphic equality: 10* speedup*)
+fun mem_stamp (_:string ref, []) = false
+  | mem_stamp (x, y::xs) = x=y orelse mem_stamp(x,xs);
+
+fun subset_stamp ([], ys) = true
+  | subset_stamp (x :: xs, ys) = mem_stamp(x, ys) andalso subset_stamp(xs, ys);
+
+fun eq_set_stamp (xs, ys) =
+    xs = ys orelse (subset_stamp (xs, ys) andalso subset_stamp (ys, xs));
 
 fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true
   | is_draft _ = false;
 
-fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = s1 subset s2;
+fun subsig (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = subset_stamp(s1,s2);
 
-fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = eq_set (s1, s2);
+fun eq_sg (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = eq_set_stamp(s1,s2);
 
 (* test if same theory names are contained in signatures' stamps,
    i.e. if signatures belong to same theory but not necessarily to the same
    version of it*)
 fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
-  eq_set (pairself (map (op !)) (s1, s2));
+  eq_set_string (pairself (map (op !)) (s1, s2));
 
 
 (* consts *)