src/Pure/type.ML
changeset 8610 f0f7600b2605
parent 8406 a217b0cd304d
child 8715 2cdabe1bb350
     1.1 --- a/src/Pure/type.ML	Thu Mar 30 14:20:01 2000 +0200
     1.2 +++ b/src/Pure/type.ML	Thu Mar 30 14:20:13 2000 +0200
     1.3 @@ -58,8 +58,7 @@
     1.4  
     1.5    (*type unification*)
     1.6    exception TUNIFY
     1.7 -  val unify: type_sig -> int -> typ Vartab.table -> (typ * typ)
     1.8 -    -> typ Vartab.table * int
     1.9 +  val unify: type_sig -> int -> typ Vartab.table -> typ * typ -> typ Vartab.table * int
    1.10    val raw_unify: typ * typ -> bool
    1.11  
    1.12    (*type inference*)
    1.13 @@ -874,9 +873,7 @@
    1.14            else constrain (Var (xi, certT T)) (get_type xi)
    1.15        | decode (t as Bound _) = t
    1.16        | decode (Const (c, T)) = Const (map_const c, certT T);
    1.17 -  in
    1.18 -    decode tm
    1.19 -  end;
    1.20 +  in decode tm end;
    1.21  
    1.22  
    1.23  (* infer_types *)