1.1 --- a/src/HOL/NatDef.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/NatDef.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -628,11 +628,11 @@
     1.4          hyp_subst_tac 1,
     1.5          rewtac Least_nat_def,
     1.6          rtac (select_equality RS arg_cong RS sym) 1,
     1.7 -        safe_tac (claset()),
     1.8 +        Safe_tac,
     1.9          dtac Suc_mono 1,
    1.10          Blast_tac 1,
    1.11          cut_facts_tac [less_linear] 1,
    1.12 -        safe_tac (claset()),
    1.13 +        Safe_tac,
    1.14          atac 2,
    1.15          Blast_tac 2,
    1.16          dtac Suc_mono 1,