diff -r dd0f298b024c -r 477c05586286 src/HOL/MiniML/W.thy
--- a/src/HOL/MiniML/W.thy	Fri Jan 17 18:35:44 1997 +0100
+++ b/src/HOL/MiniML/W.thy	Fri Jan 17 18:50:04 1997 +0100
@@ -1,28 +1,38 @@
 (* Title:     HOL/MiniML/W.thy
    ID:        $Id$
-   Author:    Dieter Nazareth and Tobias Nipkow
-   Copyright  1995 TU Muenchen
+   Author:    Wolfgang Naraschewski and Tobias Nipkow
+   Copyright  1996 TU Muenchen
 
 Type inference algorithm W
 *)
 
+
 W = MiniML + 
 
 types 
-        result_W = "(subst * typ * nat)maybe"
+        result_W = "(subst * typ * nat)option"
 
 (* type inference algorithm W *)
+
 consts
-        W :: [expr, typ list, nat] => result_W
+        W :: [expr, ctxt, nat] => result_W
 
 primrec W expr
-  "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
-                          else Fail)"
-  "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
-                           Ok(s, (s n) -> t, m) )"
-  "W (App e1 e2) a n =
-                 ( (s1,t1,m1) := W e1 a n;
-                   (s2,t2,m2) := W e2 ($s1 a) m1;
-                   u := mgu ($s2 t1) (t2 -> (TVar m2));
-                   Ok( $u o $s2 o s1, $u (TVar m2), Suc m2) )"
+  "W (Var i) A n =  
+     (if i < length A then Some( id_subst,   
+	                         bound_typ_inst (%b. TVar(b+n)) (nth i A),   
+	                         n + (min_new_bound_tv (nth i A)) )  
+	              else None)"
+  
+  "W (Abs e) A n = ( (S,t,m) := W e ((FVar n)#A) (Suc n);
+                     Some( S, (S n) -> t, m) )"
+  
+  "W (App e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
+                         (S2,t2,m2) := W e2 ($S1 A) m1;
+                         U := mgu ($S2 t1) (t2 -> (TVar m2));
+                         Some( $U o $S2 o S1, U m2, Suc m2) )"
+  
+  "W (LET e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
+                         (S2,t2,m2) := W e2 ((gen ($S1 A) t1)#($S1 A)) m1;
+                         Some( $S2 o S1, t2, m2) )"
 end