src/HOL/Plain.thy

--- a/src/HOL/Plain.thy	Fri Mar 06 20:30:16 2009 +0100
+++ b/src/HOL/Plain.thy	Fri Mar 06 20:30:17 2009 +0100
@@ -9,9 +9,6 @@
   include @{text Hilbert_Choice}.
 *}
 
-instance option :: (finite) finite
-  by default (simp add: insert_None_conv_UNIV [symmetric])
-
 ML {* path_add "~~/src/HOL/Library" *}
 
 end