src/HOL/Wellfounded.thy

--- a/src/HOL/Wellfounded.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Wellfounded.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -68,7 +68,7 @@
   assumes lin: "OFCLASS('a::ord, linorder_class)"
   shows "OFCLASS('a::ord, wellorder_class)"
 using lin by (rule wellorder_class.intro)
-  (blast intro: class.wellorder_axioms.intro wf_induct_rule [OF wf])
+  (rule class.wellorder_axioms.intro, rule wf_induct_rule [OF wf], simp)
 
 lemma (in wellorder) wf:
   "wf {(x, y). x < y}"