--- a/src/HOL/Auth/Kerberos_BAN.ML Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/Auth/Kerberos_BAN.ML Fri Nov 27 17:00:30 1998 +0100
@@ -33,7 +33,6 @@
kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2);
by possibility_tac;
by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS trans_tac);
result();