src/HOL/Library/Mapping.thy

--- a/src/HOL/Library/Mapping.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Mapping.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -183,8 +183,8 @@
 definition
   "HOL.equal m1 m2 \<longleftrightarrow> (\<forall>k. lookup m1 k = lookup m2 k)"
 
-instance proof
-qed (unfold equal_mapping_def, transfer, auto)
+instance
+  by standard (unfold equal_mapping_def, transfer, auto)
 
 end