# HG changeset patch
# User wenzelm
# Date 1003089901 -7200
# Node ID 7380c9d45626df8349acec33d91e7f5a572a6bc3
# Parent  5200b3a8f6e38547bce14ee40826ad93f9a5e9fe
tuned rewrite/simplify interface;

diff -r 5200b3a8f6e3 -r 7380c9d45626 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Sun Oct 14 20:10:44 2001 +0200
+++ b/src/Pure/meta_simplifier.ML	Sun Oct 14 22:05:01 2001 +0200
@@ -44,8 +44,8 @@
   val goals_conv        : (int -> bool) -> (cterm -> thm) -> cterm -> thm
   val forall_conv       : (cterm -> thm) -> cterm -> thm
   val fconv_rule        : (cterm -> thm) -> thm -> thm
-  val full_rewrite_aux: (meta_simpset -> thm -> thm option) -> thm list -> cterm -> thm
-  val rewrite_rule_aux  : (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
+  val rewrite_aux       : (meta_simpset -> thm -> thm option) -> bool -> thm list -> cterm -> thm
+  val simplify_aux      : (meta_simpset -> thm -> thm option) -> bool -> thm list -> thm -> thm
   val rewrite_thm       : bool * bool * bool
                           -> (meta_simpset -> thm -> thm option)
                           -> meta_simpset -> thm -> thm
@@ -950,13 +950,13 @@
 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
 
 (*Rewrite a cterm*)
-fun full_rewrite_aux _ [] = (fn ct => Thm.reflexive ct)
-  | full_rewrite_aux prover thms = rewrite_cterm (true, false, false) prover (mss_of thms);
+fun rewrite_aux _ _ [] = (fn ct => Thm.reflexive ct)
+  | rewrite_aux prover full thms = rewrite_cterm (full, false, false) prover (mss_of thms);
 
 (*Rewrite a theorem*)
-fun rewrite_rule_aux _ [] = (fn th => th)
-  | rewrite_rule_aux prover thms =
-      fconv_rule (rewrite_cterm (true, false, false) prover (mss_of thms));
+fun simplify_aux _ _ [] = (fn th => th)
+  | simplify_aux prover full thms =
+      fconv_rule (rewrite_cterm (full, false, false) prover (mss_of thms));
 
 fun rewrite_thm mode prover mss = fconv_rule (rewrite_cterm mode prover mss);