tuned;

--- a/src/HOL/IMPP/Natural.thy	Tue Feb 10 20:51:43 2015 +0100
+++ b/src/HOL/IMPP/Natural.thy	Tue Feb 10 22:52:44 2015 +0100
@@ -106,8 +106,7 @@
 lemma com_det [rule_format (no_asm)]: "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)"
 apply (erule evalc.induct)
 apply (erule_tac [8] V = "<?c,s1> -c-> s2" in thin_rl)
-(*blast needs unify_search_bound = 40*)
-apply (best elim: evalc_WHILE_case)+
+apply (blast elim: evalc_WHILE_case)+
 done
 
 lemma evaln_evalc: "<c,s> -n-> t ==> <c,s> -c-> t"