changeset 10155 | 6263a4a60e38 |
parent 9941 | fe05af7ec816 |
child 10567 | e7c9900cca4d |
--- a/src/HOL/Lambda/Type.thy Wed Oct 04 21:06:01 2000 +0200 +++ b/src/HOL/Lambda/Type.thy Wed Oct 04 22:21:10 2000 +0200 @@ -454,7 +454,7 @@ apply simp apply (rule subst_type_IT) apply (rule lists.Nil - [THEN 2 lists.Cons [THEN IT.Var], unfolded foldl_Nil [THEN eq_reflection] + [THEN [2] lists.Cons [THEN IT.Var], unfolded foldl_Nil [THEN eq_reflection] foldl_Cons [THEN eq_reflection]]) apply (erule lift_IT) apply (rule typing.App)