# HG changeset patch
# User wenzelm
# Date 970690870 -7200
# Node ID 6263a4a60e38ddf8460a0d6b5dbe3a8527c45f7e
# Parent  05d6ccb2f5364022f9c2e1308dba7a98d36936df
new 'THEN' syntax;

diff -r 05d6ccb2f536 -r 6263a4a60e38 src/HOL/Lambda/Type.thy
--- 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)