1.1 --- a/src/Pure/sign.ML	Tue Jun 01 12:35:46 2004 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Jun 01 12:36:10 2004 +0200
     1.3 @@ -905,10 +905,13 @@
     1.4  (* add type constructors *)
     1.5  
     1.6  fun ext_types _ (syn, tsig, ctab, (path, spaces), data) types =
     1.7 -  let val decls = decls_of path Syntax.type_name types in
     1.8 -    (map_syntax (Syntax.extend_type_gram types) syn,
     1.9 -      Type.add_types decls tsig, ctab,
    1.10 -      (path, add_names spaces typeK (map fst decls)), data)
    1.11 +  let
    1.12 +    val decls = decls_of path Syntax.type_name types;
    1.13 +    val tsig' = Type.add_types decls tsig;
    1.14 +    val log_types = Type.logical_types tsig';
    1.15 +  in
    1.16 +    (map_syntax (Syntax.extend_log_types log_types o Syntax.extend_type_gram types) syn,
    1.17 +      tsig', ctab, (path, add_names spaces typeK (map fst decls)), data)
    1.18    end;
    1.19  
    1.20  
    1.21 @@ -954,11 +957,7 @@
    1.22      fun prep_arity (c, Ss, S) =
    1.23        (if int then intrn spaces typeK c else c, map prepS Ss, prepS S);
    1.24      val tsig' = Type.add_arities (pp sg) (map prep_arity arities) tsig;
    1.25 -    val log_types = Type.logical_types tsig';
    1.26 -  in
    1.27 -    (map_syntax (Syntax.extend_log_types log_types) syn,
    1.28 -      tsig', ctab, (path, spaces), data)
    1.29 -  end;
    1.30 +  in (syn, tsig', ctab, (path, spaces), data) end;
    1.31  
    1.32  fun ext_arities arg = ext_ars true rd_sort arg;
    1.33  fun ext_arities_i arg = ext_ars false cert_sort arg;