--- a/src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -91,7 +91,7 @@
 
 datatype ('a::finite, 'b::finite) F = F 'a | F2 'b
 
-instance T :: (finite) finite by (default, transfer, auto)
+instance T :: (finite) finite by standard (transfer, auto)
 
 lift_definition(code_dt) f17 :: "bool \<Rightarrow> (bool T, 'b::finite) F" is "\<lambda>b. F b" by auto