1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Jul 07 07:56:24 2009 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jul 07 17:37:00 2009 +0200
     1.3 @@ -105,15 +105,9 @@
     1.4    This can be accomplished by applying the following transformation rules:
     1.5  *}
     1.6  
     1.7 -lemma Suc_if_eq': "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
     1.8 -  f n = (if n = 0 then g else h (n - 1))"
     1.9 -  by (cases n) simp_all
    1.10 -
    1.11  lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow>
    1.12    f n \<equiv> if n = 0 then g else h (n - 1)"
    1.13 -  by (rule eq_reflection, rule Suc_if_eq')
    1.14 -    (rule meta_eq_to_obj_eq, assumption,
    1.15 -     rule meta_eq_to_obj_eq, assumption)
    1.16 +  by (rule eq_reflection) (cases n, simp_all)
    1.17  
    1.18  lemma Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
    1.19    by (cases n) simp_all
    1.20 @@ -129,14 +123,14 @@
    1.21  setup {*
    1.22  let
    1.23  
    1.24 -fun gen_remove_suc Suc_if_eq dest_judgement thy thms =
    1.25 +fun remove_suc thy thms =
    1.26    let
    1.27      val vname = Name.variant (map fst
    1.28        (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "n";
    1.29      val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
    1.30      fun lhs_of th = snd (Thm.dest_comb
    1.31 -      (fst (Thm.dest_comb (dest_judgement (cprop_of th)))));
    1.32 -    fun rhs_of th = snd (Thm.dest_comb (dest_judgement (cprop_of th)));
    1.33 +      (fst (Thm.dest_comb (cprop_of th))));
    1.34 +    fun rhs_of th = snd (Thm.dest_comb (cprop_of th));
    1.35      fun find_vars ct = (case term_of ct of
    1.36          (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
    1.37        | _ $ _ =>
    1.38 @@ -156,7 +150,7 @@
    1.39               (Drule.instantiate'
    1.40                 [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
    1.41                   SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
    1.42 -               Suc_if_eq)) (Thm.forall_intr cv' th)
    1.43 +               @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
    1.44        in
    1.45          case map_filter (fn th'' =>
    1.46              SOME (th'', singleton
    1.47 @@ -169,21 +163,19 @@
    1.48        end
    1.49    in get_first mk_thms eqs end;
    1.50  
    1.51 -fun gen_eqn_suc_preproc Suc_if_eq dest_judgement dest_lhs thy thms =
    1.52 +fun eqn_suc_preproc thy thms =
    1.53    let
    1.54 -    val dest = dest_lhs o prop_of;
    1.55 +    val dest = fst o Logic.dest_equals o prop_of;
    1.56      val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
    1.57    in
    1.58      if forall (can dest) thms andalso exists (contains_suc o dest) thms
    1.59 -      then perhaps_loop (gen_remove_suc Suc_if_eq dest_judgement thy) thms
    1.60 +      then perhaps_loop (remove_suc thy) thms
    1.61         else NONE
    1.62    end;
    1.63  
    1.64 -val eqn_suc_preproc = Code_Preproc.simple_functrans (gen_eqn_suc_preproc
    1.65 -  @{thm Suc_if_eq} I (fst o Logic.dest_equals));
    1.66 +val eqn_suc_preproc1 = Code_Preproc.simple_functrans eqn_suc_preproc;
    1.67  
    1.68 -fun eqn_suc_preproc' thy thms = gen_eqn_suc_preproc
    1.69 -  @{thm Suc_if_eq'} (snd o Thm.dest_comb) (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) thy thms
    1.70 +fun eqn_suc_preproc2 thy thms = eqn_suc_preproc thy thms
    1.71    |> the_default thms;
    1.72  
    1.73  fun remove_suc_clause thy thms =
    1.74 @@ -227,9 +219,9 @@
    1.75    end;
    1.76  in
    1.77  
    1.78 -  Codegen.add_preprocessor eqn_suc_preproc'
    1.79 +  Codegen.add_preprocessor eqn_suc_preproc2
    1.80    #> Codegen.add_preprocessor clause_suc_preproc
    1.81 -  #> Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
    1.82 +  #> Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc1)
    1.83  
    1.84  end;
    1.85  *}

     2.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue Jul 07 07:56:24 2009 +0200
     2.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Jul 07 17:37:00 2009 +0200
     2.3 @@ -33,14 +33,6 @@
     2.4          |> Code.add_eqn thm'
     2.5        end;
     2.6  
     2.7 -fun meta_eq_to_obj_eq thy thm =
     2.8 -  let
     2.9 -    val T = (fastype_of o fst o Logic.dest_equals o Thm.prop_of) thm;
    2.10 -  in if Sign.of_sort thy (T, @{sort type})
    2.11 -    then SOME (Conv.fconv_rule Drule.beta_eta_conversion (@{thm meta_eq_to_obj_eq} OF [thm]))
    2.12 -    else NONE
    2.13 -  end;
    2.14 -
    2.15  fun expand_eta thy [] = []
    2.16    | expand_eta thy (thms as thm :: _) =
    2.17        let
    2.18 @@ -57,12 +49,11 @@
    2.19      val thms = Code.these_eqns thy c'
    2.20        |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    2.21        |> expand_eta thy
    2.22 -      |> map_filter (meta_eq_to_obj_eq thy)
    2.23        |> Code.norm_varnames thy
    2.24        |> map (rpair opt_name)
    2.25    in if null thms then NONE else SOME thms end;
    2.26  
    2.27 -val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
    2.28 +val dest_eqn = Logic.dest_equals;
    2.29  val const_of = dest_Const o head_of o fst o dest_eqn;
    2.30  
    2.31  fun get_equations thy defs (s, T) =