# HG changeset patch
# User wenzelm
# Date 760712974 -3600
# Node ID 3fe01df1a614fe944c5afa7b1c158af9644d52b7
# Parent  443dc2c3758378b49e12140ab9e44adecdf915f4
improved eq_sg;
cosmetical change in print_sg;

diff -r 443dc2c37583 -r 3fe01df1a614 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Feb 08 14:08:38 1994 +0100
+++ b/src/Pure/sign.ML	Tue Feb 08 14:09:34 1994 +0100
@@ -72,7 +72,7 @@
 
 fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = s1 subset s2;
 
-fun eq_sg (sg1, sg2) = subsig (sg1, sg2) andalso subsig (sg2, sg1);
+fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = eq_set (s1, s2);
 
 
 
@@ -107,7 +107,7 @@
     fun pretty_coreg (ty, ars) = map (pretty_arity ty) ars;
 
     fun pretty_const syn (c, ty) = Pretty.block
-      [Pretty.str (c ^ " ::"), Pretty.brk 1, prt_typ syn ty];
+      [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ syn ty];
 
 
     val Sg {tsig, const_tab, syn, stamps} = sg;