src/HOL/Library/Efficient_Nat.thy

 (*  Title:      HOL/Library/Efficient_Nat.thy
-    ID:         $Id$
     Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
 *)
 
 header {* Implementation of natural numbers by target-language integers *}
 

   end;
 
 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
     then remove_suc thy ths else ths
   end;

 fun clause_suc_preproc thy ths =
   let
     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;
 
 fun lift f thy eqns1 =