# HG changeset patch
# User wenzelm
# Date 954418813 -7200
# Node ID f0f7600b26058be7f0882f26e7b19c6564117a43
# Parent  ec57bc9340e8820e1f271f51ebe2938319522463
tuned;

diff -r ec57bc9340e8 -r f0f7600b2605 src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Mar 30 14:20:01 2000 +0200
+++ b/src/Pure/type.ML	Thu Mar 30 14:20:13 2000 +0200
@@ -58,8 +58,7 @@
 
   (*type unification*)
   exception TUNIFY
-  val unify: type_sig -> int -> typ Vartab.table -> (typ * typ)
-    -> typ Vartab.table * int
+  val unify: type_sig -> int -> typ Vartab.table -> typ * typ -> typ Vartab.table * int
   val raw_unify: typ * typ -> bool
 
   (*type inference*)
@@ -874,9 +873,7 @@
           else constrain (Var (xi, certT T)) (get_type xi)
       | decode (t as Bound _) = t
       | decode (Const (c, T)) = Const (map_const c, certT T);
-  in
-    decode tm
-  end;
+  in decode tm end;
 
 
 (* infer_types *)