# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID 47f283fcf2ae155c329d91d324499e7182a63c17
# Parent  a37095d030748ade5aeffeea487506f409ee38a3
Metis doesn't find an old proof in acceptable time now that higher-order equality reasoning is supported -- tuned proof script to help it

diff -r a37095d03074 -r 47f283fcf2ae src/HOL/Auth/Kerberos_BAN.thy
--- a/src/HOL/Auth/Kerberos_BAN.thy	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy	Thu May 12 15:29:19 2011 +0200
@@ -288,7 +288,8 @@
 apply (unfold before_def)
 apply (erule rev_mp)
 apply (erule bankerberos.induct, simp_all add: takeWhile_tail)
-apply (metis length_rev set_rev takeWhile_void used_evs_rev)
+apply auto
+ apply (metis length_rev set_rev takeWhile_void used_evs_rev)+
 done