fixed misfeature in Sign.extend: types of consts were read wrt. the new syntax;
authorwenzelm
Fri, 04 Mar 1994 12:14:21 +0100
changeset 277 4abe17e92130
parent 276 4cf7139e5b7a
child 278 523518f44286
fixed misfeature in Sign.extend: types of consts were read wrt. the new syntax;
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");