Added optimization: do nothing for empty list
authorpaulson
Fri Feb 14 10:41:02 1997 +0100 (1997-02-14)
changeset 2617b94dadf5b6be
parent 2616 704b6c7432cf
child 2618 15451c558a32
Added optimization: do nothing for empty list
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Fri Feb 14 10:40:23 1997 +0100
     1.2 +++ b/src/Pure/type.ML	Fri Feb 14 10:41:02 1997 +0100
     1.3 @@ -327,7 +327,8 @@
     1.4    in map_type_tvar inst end;
     1.5  
     1.6  (*Instantiation of type variables in terms *)
     1.7 -fun inst_term_tvars(tsig, tye) = map_term_types (inst_typ_tvars(tsig, tye));
     1.8 +fun inst_term_tvars (_,[]) t = t
     1.9 +  | inst_term_tvars arg    t = map_term_types (inst_typ_tvars arg) t;
    1.10  
    1.11  
    1.12  (* norm_typ *)