# HG changeset patch
# User haftmann
# Date 1176272893 -7200
# Node ID 59c117a0bcf3547228225fabe69d7c655525b298
# Parent  7ae5a6ab7bd63d570c8e6b5a25dae3a5c309b03d
dropped legacy ML bindings

diff -r 7ae5a6ab7bd6 -r 59c117a0bcf3 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