src/HOL/Datatype.thy

--- a/src/HOL/Datatype.thy	Wed Apr 11 04:13:06 2007 +0200
+++ b/src/HOL/Datatype.thy	Wed Apr 11 08:28:13 2007 +0200
@@ -763,12 +763,4 @@
 code_reserved OCaml
   option None Some
 
-
-subsection {* Basic ML bindings *}
-
-ML {*
-val not_None_eq = thm "not_None_eq";
-val not_Some_eq = thm "not_Some_eq";
-*}
-
 end