src/HOL/Library/Efficient_Nat.thy

--- a/src/HOL/Library/Efficient_Nat.thy	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Wed Dec 31 18:53:16 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Library/Efficient_Nat.thy
-    ID:         $Id$
     Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
 *)
 
@@ -170,7 +169,7 @@
 fun eqn_suc_preproc thy ths =
   let
     val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
-    fun contains_suc t = member (op =) (term_consts t) @{const_name Suc};
+    fun contains_suc t = member (op =) (OldTerm.term_consts t) @{const_name Suc};
   in
     if forall (can dest) ths andalso
       exists (contains_suc o dest) ths
@@ -212,7 +211,7 @@
     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
+      exists (fn th => member (op =) (foldr OldTerm.add_term_consts
         [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths
     then remove_suc_clause thy ths else ths
   end;