# HG changeset patch
# User wenzelm
# Date 1369912043 -7200
# Node ID a2d4ae3e04a2ffd8aaf9e1df293170b0eb01f5e8
# Parent  cc30c4eb4ec93127d808b7f66769f067bedb63e9
tuned signature;

diff -r cc30c4eb4ec9 -r a2d4ae3e04a2 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Thu May 30 12:56:25 2013 +0200
+++ b/src/Pure/Isar/object_logic.ML	Thu May 30 13:07:23 2013 +0200
@@ -201,7 +201,7 @@
 fun rulify_tac i st = rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
 
 fun gen_rulify full thm =
-  Raw_Simplifier.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
+  Conv.fconv_rule (Raw_Simplifier.rewrite full (get_rulify (Thm.theory_of_thm thm))) thm
   |> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes;
 
 val rulify = gen_rulify true;
diff -r cc30c4eb4ec9 -r a2d4ae3e04a2 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Thu May 30 12:56:25 2013 +0200
+++ b/src/Pure/raw_simplifier.ML	Thu May 30 13:07:23 2013 +0200
@@ -129,7 +129,6 @@
   val generic_rewrite_goal_tac: bool * bool * bool ->
     (Proof.context -> tactic) -> Proof.context -> int -> tactic
   val rewrite: bool -> thm list -> conv
-  val simplify: bool -> thm list -> thm -> thm
 end;
 
 structure Raw_Simplifier: RAW_SIMPLIFIER =
@@ -1329,8 +1328,7 @@
       rewrite_cterm (full, false, false) simple_prover
         (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
 
-fun simplify full thms = Conv.fconv_rule (rewrite full thms);
-val rewrite_rule = simplify true;
+val rewrite_rule = Conv.fconv_rule o rewrite true;
 
 (*simple term rewriting -- no proof*)
 fun rewrite_term thy rules procs =