Removed "code del" declarations again.

--- a/src/HOL/Library/EfficientNat.thy	Thu Jun 08 15:25:07 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Thu Jun 08 17:04:49 2006 +0200
@@ -85,13 +85,6 @@
 using their counterparts on the integers:
 *}
 
-declare
-  Nat.plus.simps [code del]
-  Nat.minus.simps [code del]
-  diff_0_eq_0 [code del]
-  diff_Suc_Suc [code del]
-  Nat.times.simps [code del]
-
 lemma [code]: "m + n = nat (int m + int n)"
   by arith
 lemma [code]: "m - n = nat (int m - int n)"
@@ -218,7 +211,7 @@
               (Drule.instantiate' []
                 [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
                    abstract_over (Sucv,
-                     (HOLogic.dest_Trueprop o prop_of) th'))))),
+                     HOLogic.dest_Trueprop (prop_of th')))))),
                  SOME (cert v)] Suc_clause'))
             (Thm.forall_intr (cert v) th'))
         in
@@ -229,7 +222,7 @@
 
 fun clause_suc_preproc thy ths =
   let
-    val dest = fst o HOLogic.dest_mem o ObjectLogic.drop_judgment thy
+    val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
   in
     if forall (can (dest o concl_of)) ths andalso
       exists (fn th => member (op =) (foldr add_term_consts