src/CCL/Wfd.thy

--- a/src/CCL/Wfd.thy	Thu Jun 21 20:48:48 2007 +0200
+++ b/src/CCL/Wfd.thy	Thu Jun 21 22:10:16 2007 +0200
@@ -340,7 +340,11 @@
   apply (rule 3)
     apply (rule 1 [symmetric])
   apply (rule rcall2T)
-      apply assumption+
+      apply (rule 2)
+     apply assumption
+    apply (rule 4)
+   apply (rule 5)
+  apply (rule 6)
   done
 
 lemma hyprcall3T:
@@ -355,7 +359,12 @@
   apply (rule 3)
    apply (rule 1 [symmetric])
   apply (rule rcall3T)
-  apply assumption+
+       apply (rule 2)
+      apply assumption
+     apply (rule 4)
+    apply (rule 5)
+   apply (rule 6)
+  apply (rule 7)
   done
 
 lemmas hyprcallTs = hyprcallT hyprcall2T hyprcall3T