1.1 --- a/src/Pure/Isar/object_logic.ML	Thu May 30 12:56:25 2013 +0200
     1.2 +++ b/src/Pure/Isar/object_logic.ML	Thu May 30 13:07:23 2013 +0200
     1.3 @@ -201,7 +201,7 @@
     1.4  fun rulify_tac i st = rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
     1.5  
     1.6  fun gen_rulify full thm =
     1.7 -  Raw_Simplifier.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
     1.8 +  Conv.fconv_rule (Raw_Simplifier.rewrite full (get_rulify (Thm.theory_of_thm thm))) thm
     1.9    |> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes;
    1.10  
    1.11  val rulify = gen_rulify true;

     2.1 --- a/src/Pure/raw_simplifier.ML	Thu May 30 12:56:25 2013 +0200
     2.2 +++ b/src/Pure/raw_simplifier.ML	Thu May 30 13:07:23 2013 +0200
     2.3 @@ -129,7 +129,6 @@
     2.4    val generic_rewrite_goal_tac: bool * bool * bool ->
     2.5      (Proof.context -> tactic) -> Proof.context -> int -> tactic
     2.6    val rewrite: bool -> thm list -> conv
     2.7 -  val simplify: bool -> thm list -> thm -> thm
     2.8  end;
     2.9  
    2.10  structure Raw_Simplifier: RAW_SIMPLIFIER =
    2.11 @@ -1329,8 +1328,7 @@
    2.12        rewrite_cterm (full, false, false) simple_prover
    2.13          (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
    2.14  
    2.15 -fun simplify full thms = Conv.fconv_rule (rewrite full thms);
    2.16 -val rewrite_rule = simplify true;
    2.17 +val rewrite_rule = Conv.fconv_rule o rewrite true;
    2.18  
    2.19  (*simple term rewriting -- no proof*)
    2.20  fun rewrite_term thy rules procs =