src/HOL/HOLCF/Completion.thy

--- a/src/HOL/HOLCF/Completion.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Completion.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -116,7 +116,7 @@
   assumes type: "type_definition Rep Abs {S. ideal S}"
   assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
   shows "OFCLASS('b, cpo_class)"
-by (default, rule exI, erule typedef_ideal_lub [OF type below])
+  by standard (rule exI, erule typedef_ideal_lub [OF type below])
 
 end