1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Mon Feb 16 13:38:08 2009 +0100
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Mon Feb 16 13:38:09 2009 +0100
     1.3 @@ -107,10 +107,10 @@
     1.4  
     1.5  lemma Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
     1.6    f n = (if n = 0 then g else h (n - 1))"
     1.7 -  by (case_tac n) simp_all
     1.8 +  by (cases n) simp_all
     1.9  
    1.10  lemma Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
    1.11 -  by (case_tac n) simp_all
    1.12 +  by (cases n) simp_all
    1.13  
    1.14  text {*
    1.15    The rules above are built into a preprocessor that is plugged into
    1.16 @@ -132,7 +132,7 @@
    1.17        (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
    1.18      fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
    1.19      fun find_vars ct = (case term_of ct of
    1.20 -        (Const ("Suc", _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
    1.21 +        (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
    1.22        | _ $ _ =>
    1.23          let val (ct1, ct2) = Thm.dest_comb ct
    1.24          in 
    1.25 @@ -236,7 +236,6 @@
    1.26    Codegen.add_preprocessor eqn_suc_preproc
    1.27    #> Codegen.add_preprocessor clause_suc_preproc
    1.28    #> Code.add_functrans ("eqn_Suc", lift eqn_suc_preproc)
    1.29 -  #> Code.add_functrans ("clause_Suc", lift clause_suc_preproc)
    1.30  
    1.31  end;
    1.32  *}