diff -r d760049b2d18 -r a360406f1fcb 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