diff -r 1f00494e37a5 -r 5d909faf0e04 src/HOL/MiniML/I.thy
--- a/src/HOL/MiniML/I.thy	Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/I.thy	Fri Dec 08 19:48:15 1995 +0100
@@ -8,17 +8,16 @@
 I = W +
 
 consts
-	I :: [expr, type_expr list, nat, subst] => result_W
+	I :: [expr, typ list, nat, subst] => result_W
 
 primrec I expr
         I_Var	"I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
                                     else Fail)"
-        I_Abs	"I (Abs e) a n s = I e ((TVar n)#a) (Suc n) s   bind
-                                   (%(s,t,m). Ok(s, Fun (TVar n) t, m) )"
+        I_Abs	"I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
+                                     Ok(s, TVar n -> t, m) )"
         I_App	"I (App e1 e2) a n s =
- 		 I e1 a n s   bind
-		 (%(s1,t1,m1). I e2 a m1 s1  bind   
-		 (%(s2,t2,m2). mgu ($s2 t1) (Fun ($s2 t2) (TVar m2)) bind
-		 (%u. Ok($u o s2, TVar m2, Suc m2) ) ))"
-
+ 		   ( (s1,t1,m1) := I e1 a n s;
+		     (s2,t2,m2) := I e2 a m1 s1;
+		     u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
+		     Ok($u o s2, TVar m2, Suc m2) )"
 end