# HG changeset patch
# User wenzelm
# Date 762779661 -3600
# Node ID 4abe17e921300cdee6677f51f76f9acde28e0231
# Parent  4cf7139e5b7afbec5bb5f958df96f63e9e532dc0
fixed misfeature in Sign.extend: types of consts were read wrt. the new syntax;

diff -r 4cf7139e5b7a -r 4abe17e92130 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Mar 03 17:43:14 1994 +0100
+++ b/src/Pure/sign.ML	Fri Mar 04 12:14:21 1994 +0100
@@ -245,8 +245,8 @@
     val all_consts = flat (map (fn (cs, s) => map (rpair s) cs)
       (Syntax.constants sext @ consts));
 
-    val const_tab1 =                              (* FIXME bug: vvvv should be syn *)
-      Symtab.extend (K false) (const_tab, map (read_const tsig1 syn1) all_consts)
+    val const_tab1 =
+      Symtab.extend (K false) (const_tab, map (read_const tsig1 syn) all_consts)
         handle Symtab.DUPLICATE c
           => error ("Constant " ^ quote c ^ " declared twice");