--- a/src/HOL/IMP/VC.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/IMP/VC.thy Wed Mar 19 22:50:42 2008 +0100
@@ -77,7 +77,7 @@
apply fast
(* if *)
apply atomize
- apply (tactic "Deepen_tac 4 1")
+ apply (tactic "deepen_tac @{claset} 4 1")
(* while *)
apply atomize
apply (intro allI impI)