--- 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;
--- 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 =