src/HOL/IMP/Abs_Int2.thy

--- a/src/HOL/IMP/Abs_Int2.thy	Wed Jul 02 17:34:45 2014 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy	Wed Jun 11 14:24:23 2014 +1000
@@ -132,8 +132,10 @@
     by simp (metis And(1) And(2) in_gamma_sup_UpI)
 next
   case (Less e1 e2) thus ?case
-    by(auto split: prod.split)
-      (metis (lifting) inv_aval'_correct aval''_correct inv_less')
+    apply hypsubst_thin
+    apply (auto split: prod.split)
+    apply (metis (lifting) inv_aval'_correct aval''_correct inv_less')
+    done
 qed
 
 definition "step' = Step