# HG changeset patch
# User bulwahn
# Date 1319008276 -7200
# Node ID 645c6cac779e91f5908b4807b4fc6e2186eaca0b
# Parent  3a0c63c0ed48c6aef7f4d630da632f46049c0973
removing old code generator setup for executable sets

diff -r 3a0c63c0ed48 -r 645c6cac779e src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Wed Oct 19 09:11:15 2011 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Wed Oct 19 09:11:16 2011 +0200
@@ -41,13 +41,6 @@
 
 code_datatype Set Coset
 
-consts_code
-  Coset ("\<module>Coset")
-  Set ("\<module>Set")
-attach {*
-  datatype 'a set = Set of 'a list | Coset of 'a list;
-*} -- {* This assumes that there won't be a @{text Coset} without a @{text Set} *}
-
 
 subsection {* Basic operations *}