src/HOL/Limits.thy

--- a/src/HOL/Limits.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Limits.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -710,13 +710,15 @@
 
 lemma (in bounded_bilinear) flip:
   "bounded_bilinear (\<lambda>x y. y ** x)"
-  apply default
+  apply standard
   apply (rule add_right)
   apply (rule add_left)
   apply (rule scaleR_right)
   apply (rule scaleR_left)
   apply (subst mult.commute)
-  using bounded by fast
+  using bounded
+  apply fast
+  done
 
 lemma (in bounded_bilinear) Bfun_prod_Zfun:
   assumes f: "Bfun f F"