# HG changeset patch
# User wenzelm
# Date 1082624102 -7200
# Node ID 3224082514f9abf8946ee036c1496397914a7e62
# Parent  130076a81b8414e5101ca0eb61318d8f524b9931
adapted Sign.rep_sg;

diff -r 130076a81b84 -r 3224082514f9 src/Pure/display.ML
--- a/src/Pure/display.ML	Thu Apr 22 10:52:32 2004 +0200
+++ b/src/Pure/display.ML	Thu Apr 22 10:55:02 2004 +0200
@@ -224,7 +224,7 @@
     fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
 
 
-    val {self = _, tsig, const_tab, syn = _, path, spaces, data} = Sign.rep_sg sg;
+    val {self = _, tsig, const_tab, path, spaces, data} = Sign.rep_sg sg;
     val {axioms, oracles, ...} = Theory.rep_theory thy;
     val spaces' = Library.sort_wrt fst spaces;
     val {classes, classrel, default, tycons = type_tab, log_types, univ_witness, abbrs, arities} =