# HG changeset patch
# User haftmann
# Date 1159822858 -7200
# Node ID 5e92606245b652e3285a8418aaf8d897072b8750
# Parent  ed49d8709959540a8ba6003e6f8281f7e91daa6e
added code for insert

diff -r ed49d8709959 -r 5e92606245b6 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Mon Oct 02 23:00:57 2006 +0200
+++ b/src/HOL/Library/ExecutableSet.thy	Mon Oct 02 23:00:58 2006 +0200
@@ -282,6 +282,10 @@
   (SML "{*insertl*}")
   (Haskell "{*insertl*}")
 
+code_const insert
+  (SML "{*insertl*}")
+  (Haskell "{*insertl*}")
+
 code_const "op \<union>"
   (SML "{*unionl*}")
   (Haskell "{*unionl*}")