src/HOL/Library/List_Prefix.thy

 imports List
 begin
 
 subsection {* Prefix order on lists *}
 
-instance list :: (type) ord ..
-
-defs (overloaded)
-  prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs"
-  strict_prefix_def: "xs < ys == xs \<le> ys \<and> xs \<noteq> (ys::'a list)"
-
-instance list :: (type) order
+instantiation list :: (type) order
+begin
+
+definition
+  prefix_def [code func del]: "xs \<le> ys = (\<exists>zs. ys = xs @ zs)"
+
+definition
+  strict_prefix_def [code func del]: "xs < ys = (xs \<le> ys \<and> xs \<noteq> (ys::'a list))"
+
+instance
   by intro_classes (auto simp add: prefix_def strict_prefix_def)
+
+end
 
 lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"
   unfolding prefix_def by blast
 
 lemma prefixE [elim?]: