src/HOL/Lambda/Type.thy
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)