# HG changeset patch
# User wenzelm
# Date 1183658495 -7200
# Node ID e03a43b8178c88f110aebe85bf55388d7e05f8de
# Parent  ab67175ca8a56e76d1232b8c48ed2ea53f6564e9
tuned;

diff -r ab67175ca8a5 -r e03a43b8178c src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Thu Jul 05 20:01:34 2007 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu Jul 05 20:01:35 2007 +0200
@@ -107,8 +107,7 @@
   val debug_bounds: bool ref
   val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
   val set_solvers: solver list -> simpset -> simpset
-  val rewrite_cterm: bool * bool * bool ->
-    (simpset -> thm -> thm option) -> simpset -> cterm -> thm
+  val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv
   val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
   val rewrite_thm: bool * bool * bool ->
     (simpset -> thm -> thm option) -> simpset -> thm -> thm
@@ -118,7 +117,7 @@
     (simpset -> tactic) -> simpset -> int -> tactic
   val norm_hhf: thm -> thm
   val norm_hhf_protect: thm -> thm
-  val rewrite: bool -> thm list -> cterm -> thm
+  val rewrite: bool -> thm list -> conv
   val simplify: bool -> thm list -> thm -> thm
 end;
 
@@ -1256,11 +1255,7 @@
         (theory_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
 
 (*Rewrite a theorem*)
-fun simplify _ [] th = th
-  | simplify full thms th =
-      Conv.fconv_rule (rewrite_cterm (full, false, false) simple_prover
-        (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms)) th;
-
+fun simplify full thms = Conv.fconv_rule (rewrite full thms);
 val rewrite_rule = simplify true;
 
 (*simple term rewriting -- no proof*)
diff -r ab67175ca8a5 -r e03a43b8178c src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Jul 05 20:01:34 2007 +0200
+++ b/src/Pure/simplifier.ML	Thu Jul 05 20:01:35 2007 +0200
@@ -55,11 +55,11 @@
     -> (theory -> simpset -> term -> thm option) -> simproc
   val simproc: theory -> string -> string list
     -> (theory -> simpset -> term -> thm option) -> simproc
-  val          rewrite: simpset -> cterm -> thm
-  val      asm_rewrite: simpset -> cterm -> thm
-  val     full_rewrite: simpset -> cterm -> thm
-  val   asm_lr_rewrite: simpset -> cterm -> thm
-  val asm_full_rewrite: simpset -> cterm -> thm
+  val          rewrite: simpset -> conv
+  val      asm_rewrite: simpset -> conv
+  val     full_rewrite: simpset -> conv
+  val   asm_lr_rewrite: simpset -> conv
+  val asm_full_rewrite: simpset -> conv
   val get_simpset: theory -> simpset
   val print_local_simpset: Proof.context -> unit
   val get_local_simpset: Proof.context -> simpset