# HG changeset patch
# User haftmann
# Date 1266477432 -3600
# Node ID 6eab566aa609a71319703722de5f62af9f27b58b
# Parent  5163c2d009046b089036e12fd82fdd60b66588de
drop code lemma for ordered_keys

diff -r 5163c2d00904 -r 6eab566aa609 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Wed Feb 17 16:49:38 2010 +0100
+++ b/src/HOL/Library/Tree.thy	Thu Feb 18 08:17:12 2010 +0100
@@ -124,6 +124,9 @@
   "Mapping.update k v (Tree t) = Tree (update k v t)"
   by (simp add: Tree_def lookup_update)
 
+lemma [code, code del]:
+  "Mapping.ordered_keys = Mapping.ordered_keys " ..
+
 lemma keys_Tree [code]:
   "Mapping.keys (Tree t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
   by (simp add: Mapping.keys_def lookup_Tree dom_lookup)