src/HOL/MicroJava/J/State.thy

--- a/src/HOL/MicroJava/J/State.thy	Sat Apr 07 17:55:35 2012 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Sat Apr 07 18:08:29 2012 +0200
@@ -190,9 +190,12 @@
 apply simp
 done
 
-instantiation loc' :: equal begin
+instantiation loc' :: equal
+begin
+
 definition "HOL.equal (l :: loc') l' \<longleftrightarrow> l = l'"
-instance proof qed(simp add: equal_loc'_def)
+instance by default (simp add: equal_loc'_def)
+
 end
 
 end