fixed misfeature in Sign.extend: types of consts were read wrt. the new syntax;
authorwenzelm
Fri Mar 04 12:14:21 1994 +0100 (1994-03-04)
changeset 2774abe17e92130
parent 276 4cf7139e5b7a
child 278 523518f44286
fixed misfeature in Sign.extend: types of consts were read wrt. the new syntax;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Thu Mar 03 17:43:14 1994 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Mar 04 12:14:21 1994 +0100
     1.3 @@ -245,8 +245,8 @@
     1.4      val all_consts = flat (map (fn (cs, s) => map (rpair s) cs)
     1.5        (Syntax.constants sext @ consts));
     1.6  
     1.7 -    val const_tab1 =                              (* FIXME bug: vvvv should be syn *)
     1.8 -      Symtab.extend (K false) (const_tab, map (read_const tsig1 syn1) all_consts)
     1.9 +    val const_tab1 =
    1.10 +      Symtab.extend (K false) (const_tab, map (read_const tsig1 syn) all_consts)
    1.11          handle Symtab.DUPLICATE c
    1.12            => error ("Constant " ^ quote c ^ " declared twice");
    1.13