diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Sublist.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -18,10 +18,10 @@
   where "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
 
 interpretation prefix_order: order prefixeq prefix
-  by default (auto simp: prefixeq_def prefix_def)
+  by standard (auto simp: prefixeq_def prefix_def)
 
 interpretation prefix_bot: order_bot Nil prefixeq prefix
-  by default (simp add: prefixeq_def)
+  by standard (simp add: prefixeq_def)
 
 lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
   unfolding prefixeq_def by blast