--- a/src/HOL/W0/W.thy Mon Dec 29 21:39:22 1997 +0100
+++ b/src/HOL/W0/W.thy Tue Dec 30 11:14:09 1997 +0100
@@ -16,10 +16,10 @@
W :: [expr, typ list, 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 (Var i) a n = (if i < length a then Ok(id_subst, a!i, n)
+ else Fail)"
"W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
- Ok(s, (s n) -> t, m) )"
+ 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;