src/HOL/Auth/Kerberos_BAN_Gets.thy

--- a/src/HOL/Auth/Kerberos_BAN_Gets.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -288,7 +288,7 @@
 apply (blast dest: used_evs_rev [THEN equalityD2, THEN contra_subsetD] 
                    used_takeWhile_used)
 txt{*subcase: CT before*}
-apply (fastsimp dest!: set_evs_rev [THEN equalityD2, THEN contra_subsetD, THEN takeWhile_void])
+apply (fastforce dest!: set_evs_rev [THEN equalityD2, THEN contra_subsetD, THEN takeWhile_void])
 done