fixed misfeature in Sign.extend: types of consts were read wrt. the new syntax;
--- 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");