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