src/HOL/Library/Efficient_Nat.thy
changeset 29287 5b0bfd63b5da
parent 29270 0eade173f77e
child 29657 881f328dfbb3
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Thu Jan 01 14:23:38 2009 +0100
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Jan 01 14:23:39 2009 +0100
     1.3 @@ -169,7 +169,7 @@
     1.4  fun eqn_suc_preproc thy ths =
     1.5    let
     1.6      val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
     1.7 -    fun contains_suc t = member (op =) (OldTerm.term_consts t) @{const_name Suc};
     1.8 +    val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
     1.9    in
    1.10      if forall (can dest) ths andalso
    1.11        exists (contains_suc o dest) ths
    1.12 @@ -211,8 +211,8 @@
    1.13      val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
    1.14    in
    1.15      if forall (can (dest o concl_of)) ths andalso
    1.16 -      exists (fn th => member (op =) (foldr OldTerm.add_term_consts
    1.17 -        [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths
    1.18 +      exists (fn th => exists (exists_Const (fn (c, _) => c = @{const_name Suc}))
    1.19 +        (map_filter (try dest) (concl_of th :: prems_of th))) ths
    1.20      then remove_suc_clause thy ths else ths
    1.21    end;
    1.22