src/Pure/sign.ML
changeset 277 4abe17e92130
parent 267 ab78019b8ec8
child 386 e9ba9f7e2542
equal deleted inserted replaced
276:4cf7139e5b7a 277:4abe17e92130
   243       (logical_types tsig1, xconsts, sext);
   243       (logical_types tsig1, xconsts, sext);
   244 
   244 
   245     val all_consts = flat (map (fn (cs, s) => map (rpair s) cs)
   245     val all_consts = flat (map (fn (cs, s) => map (rpair s) cs)
   246       (Syntax.constants sext @ consts));
   246       (Syntax.constants sext @ consts));
   247 
   247 
   248     val const_tab1 =                              (* FIXME bug: vvvv should be syn *)
   248     val const_tab1 =
   249       Symtab.extend (K false) (const_tab, map (read_const tsig1 syn1) all_consts)
   249       Symtab.extend (K false) (const_tab, map (read_const tsig1 syn) all_consts)
   250         handle Symtab.DUPLICATE c
   250         handle Symtab.DUPLICATE c
   251           => error ("Constant " ^ quote c ^ " declared twice");
   251           => error ("Constant " ^ quote c ^ " declared twice");
   252 
   252 
   253     val stamps1 =
   253     val stamps1 =
   254       if exists (equal name o !) stamps then
   254       if exists (equal name o !) stamps then