# HG changeset patch
# User berghofe
# Date 1210150610 -7200
# Node ID 9eede540a5e86fe5bd652000a7c633c357e853a1
# Parent  244184661a097b3f40cb1be90b79b56b5747d4a8
Deleted instantiation "set :: (type) itself".

diff -r 244184661a09 -r 9eede540a5e8 src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Wed May 07 10:56:49 2008 +0200
+++ b/src/HOL/Typedef.thy	Wed May 07 10:56:50 2008 +0200
@@ -160,15 +160,6 @@
 
 end
 
-instantiation "set" :: ("type") itself
-begin
-
-definition "itself = TYPE('a set)"
-
-instance ..
-
-end
-
 hide (open) const itself
 
 end