improved eq_sg;
authorwenzelm
Tue Feb 08 14:09:34 1994 +0100 (1994-02-08)
changeset 2663fe01df1a614
parent 265 443dc2c37583
child 267 ab78019b8ec8
improved eq_sg;
cosmetical change in print_sg;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Tue Feb 08 14:08:38 1994 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Feb 08 14:09:34 1994 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4  
     1.5  fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = s1 subset s2;
     1.6  
     1.7 -fun eq_sg (sg1, sg2) = subsig (sg1, sg2) andalso subsig (sg2, sg1);
     1.8 +fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = eq_set (s1, s2);
     1.9  
    1.10  
    1.11  
    1.12 @@ -107,7 +107,7 @@
    1.13      fun pretty_coreg (ty, ars) = map (pretty_arity ty) ars;
    1.14  
    1.15      fun pretty_const syn (c, ty) = Pretty.block
    1.16 -      [Pretty.str (c ^ " ::"), Pretty.brk 1, prt_typ syn ty];
    1.17 +      [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ syn ty];
    1.18  
    1.19  
    1.20      val Sg {tsig, const_tab, syn, stamps} = sg;