src/HOL/MicroJava/J/Type.thy

 
 instantiation cnam :: equal
 begin
 
 definition "HOL.equal (cn :: cnam) cn' \<longleftrightarrow> cn = cn'"
-instance by default (simp add: equal_cnam_def)
+instance by standard (simp add: equal_cnam_def)
 
 end
 
 text {* These instantiations only ensure that the merge in theory @{text "MicroJava"} succeeds. FIXME *}
 

 
 instantiation vnam :: equal
 begin
 
 definition "HOL.equal (vn :: vnam) vn' \<longleftrightarrow> vn = vn'"
-instance by default (simp add: equal_vnam_def)
+instance by standard (simp add: equal_vnam_def)
 
 end
 
 instantiation vnam :: typerep
 begin

 
 instantiation mname :: equal
 begin
 
 definition "HOL.equal (M :: mname) M' \<longleftrightarrow> M = M'"
-instance by default (simp add: equal_mname_def)
+instance by standard (simp add: equal_mname_def)
 
 end
 
 instantiation mname :: typerep
 begin