# HG changeset patch
# User haftmann
# Date 1278084464 -7200
# Node ID 4117177327106e0df021a2718c0764c3b257fc4c
# Parent  bd90378b8171653701602fcda5dbc5bd86b80283
explicit code_datatype declaration prevents multiple instantiations later on

diff -r bd90378b8171 -r 411717732710 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Fri Jul 02 16:50:53 2010 +0200
+++ b/src/HOL/Library/Mapping.thy	Fri Jul 02 17:27:44 2010 +0200
@@ -278,6 +278,8 @@
 
 subsection {* Code generator setup *}
 
+code_datatype empty update
+
 instantiation mapping :: (type, type) eq
 begin