changeset 4502 | 337c073de95e |
parent 2525 | 477c05586286 |
child 14422 | b8da5f258b04 |
--- a/src/HOL/MiniML/MiniML.thy Mon Dec 29 21:39:22 1997 +0100 +++ b/src/HOL/MiniML/MiniML.thy Tue Dec 30 11:14:09 1997 +0100 @@ -23,7 +23,7 @@ inductive has_type intrs - VarI "[| n < length A; t <| (nth n A) |] ==> A |- Var n :: t" + VarI "[| n < length A; t <| A!n |] ==> A |- Var n :: t" AbsI "[| (mk_scheme t1)#A |- e :: t2 |] ==> A |- Abs e :: t1 -> t2" AppI "[| A |- e1 :: t2 -> t1; A |- e2 :: t2 |] ==> A |- App e1 e2 :: t1"