Removal of polymorphic equality via mem, subset, eq_set, etc
authorpaulson
Wed Nov 13 10:38:08 1996 +0100 (1996-11-13)
changeset 2180934572a94139
parent 2179 018906568ef0
child 2181 9c2b4728641d
Removal of polymorphic equality via mem, subset, eq_set, etc
src/Pure/display.ML
src/Pure/drule.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/display.ML	Tue Nov 12 13:20:36 1996 +0100
     1.2 +++ b/src/Pure/display.ML	Wed Nov 13 10:38:08 1996 +0100
     1.3 @@ -118,7 +118,7 @@
     1.4  
     1.5    fun ins_entry (x, y) [] = [(x, [y])]
     1.6      | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
     1.7 -        if x = x' then (x', y ins ys') :: pairs
     1.8 +        if x = x' then (x', y ins_string ys') :: pairs
     1.9          else pair :: ins_entry (x, y) pairs;
    1.10  
    1.11    fun add_type_env (Free (x, T), env) = ins_entry (T, x) env
     2.1 --- a/src/Pure/drule.ML	Tue Nov 12 13:20:36 1996 +0100
     2.2 +++ b/src/Pure/drule.ML	Wed Nov 13 10:38:08 1996 +0100
     2.3 @@ -461,7 +461,7 @@
     2.4      let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
     2.5          and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
     2.6      in  Sign.eq_sg (sg1,sg2) andalso
     2.7 -        eq_set (shyps1, shyps2) andalso
     2.8 +        eq_set_sort (shyps1, shyps2) andalso
     2.9          aconvs(hyps1,hyps2) andalso
    2.10          prop1 aconv prop2
    2.11      end;
    2.12 @@ -473,7 +473,7 @@
    2.13      let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
    2.14          and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
    2.15      in  Sign.same_sg (sg1,sg2) andalso
    2.16 -        eq_set (shyps1, shyps2) andalso
    2.17 +        eq_set_sort (shyps1, shyps2) andalso
    2.18          aconvs(hyps1,hyps2) andalso
    2.19          prop1 aconv prop2
    2.20      end;
     3.1 --- a/src/Pure/sign.ML	Tue Nov 12 13:20:36 1996 +0100
     3.2 +++ b/src/Pure/sign.ML	Wed Nov 13 10:38:08 1996 +0100
     3.3 @@ -88,20 +88,30 @@
     3.4  val tsig_of = #tsig o rep_sg;
     3.5  
     3.6  
     3.7 -(* stamps *)
     3.8 +(*** Stamps ***)
     3.9 +
    3.10 +(*Avoiding polymorphic equality: 10* speedup*)
    3.11 +fun mem_stamp (_:string ref, []) = false
    3.12 +  | mem_stamp (x, y::xs) = x=y orelse mem_stamp(x,xs);
    3.13 +
    3.14 +fun subset_stamp ([], ys) = true
    3.15 +  | subset_stamp (x :: xs, ys) = mem_stamp(x, ys) andalso subset_stamp(xs, ys);
    3.16 +
    3.17 +fun eq_set_stamp (xs, ys) =
    3.18 +    xs = ys orelse (subset_stamp (xs, ys) andalso subset_stamp (ys, xs));
    3.19  
    3.20  fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true
    3.21    | is_draft _ = false;
    3.22  
    3.23 -fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = s1 subset s2;
    3.24 +fun subsig (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = subset_stamp(s1,s2);
    3.25  
    3.26 -fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = eq_set (s1, s2);
    3.27 +fun eq_sg (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = eq_set_stamp(s1,s2);
    3.28  
    3.29  (* test if same theory names are contained in signatures' stamps,
    3.30     i.e. if signatures belong to same theory but not necessarily to the same
    3.31     version of it*)
    3.32  fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
    3.33 -  eq_set (pairself (map (op !)) (s1, s2));
    3.34 +  eq_set_string (pairself (map (op !)) (s1, s2));
    3.35  
    3.36  
    3.37  (* consts *)