src/HOL/Library/Efficient_Nat.thy
changeset 29270 0eade173f77e
parent 29258 bce03c644efb
child 29287 5b0bfd63b5da
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Dec 31 15:30:10 2008 +0100
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Wed Dec 31 18:53:16 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Library/Efficient_Nat.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
     1.7  *)
     1.8  
     1.9 @@ -170,7 +169,7 @@
    1.10  fun eqn_suc_preproc thy ths =
    1.11    let
    1.12      val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
    1.13 -    fun contains_suc t = member (op =) (term_consts t) @{const_name Suc};
    1.14 +    fun contains_suc t = member (op =) (OldTerm.term_consts t) @{const_name Suc};
    1.15    in
    1.16      if forall (can dest) ths andalso
    1.17        exists (contains_suc o dest) ths
    1.18 @@ -212,7 +211,7 @@
    1.19      val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
    1.20    in
    1.21      if forall (can (dest o concl_of)) ths andalso
    1.22 -      exists (fn th => member (op =) (foldr add_term_consts
    1.23 +      exists (fn th => member (op =) (foldr OldTerm.add_term_consts
    1.24          [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths
    1.25      then remove_suc_clause thy ths else ths
    1.26    end;