src/Pure/meta_simplifier.ML
changeset 11767 7380c9d45626
parent 11760 8e906f051fbc
child 11886 36d0585f87de
     1.1 --- a/src/Pure/meta_simplifier.ML	Sun Oct 14 20:10:44 2001 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Sun Oct 14 22:05:01 2001 +0200
     1.3 @@ -44,8 +44,8 @@
     1.4    val goals_conv        : (int -> bool) -> (cterm -> thm) -> cterm -> thm
     1.5    val forall_conv       : (cterm -> thm) -> cterm -> thm
     1.6    val fconv_rule        : (cterm -> thm) -> thm -> thm
     1.7 -  val full_rewrite_aux: (meta_simpset -> thm -> thm option) -> thm list -> cterm -> thm
     1.8 -  val rewrite_rule_aux  : (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
     1.9 +  val rewrite_aux       : (meta_simpset -> thm -> thm option) -> bool -> thm list -> cterm -> thm
    1.10 +  val simplify_aux      : (meta_simpset -> thm -> thm option) -> bool -> thm list -> thm -> thm
    1.11    val rewrite_thm       : bool * bool * bool
    1.12                            -> (meta_simpset -> thm -> thm option)
    1.13                            -> meta_simpset -> thm -> thm
    1.14 @@ -950,13 +950,13 @@
    1.15  fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
    1.16  
    1.17  (*Rewrite a cterm*)
    1.18 -fun full_rewrite_aux _ [] = (fn ct => Thm.reflexive ct)
    1.19 -  | full_rewrite_aux prover thms = rewrite_cterm (true, false, false) prover (mss_of thms);
    1.20 +fun rewrite_aux _ _ [] = (fn ct => Thm.reflexive ct)
    1.21 +  | rewrite_aux prover full thms = rewrite_cterm (full, false, false) prover (mss_of thms);
    1.22  
    1.23  (*Rewrite a theorem*)
    1.24 -fun rewrite_rule_aux _ [] = (fn th => th)
    1.25 -  | rewrite_rule_aux prover thms =
    1.26 -      fconv_rule (rewrite_cterm (true, false, false) prover (mss_of thms));
    1.27 +fun simplify_aux _ _ [] = (fn th => th)
    1.28 +  | simplify_aux prover full thms =
    1.29 +      fconv_rule (rewrite_cterm (full, false, false) prover (mss_of thms));
    1.30  
    1.31  fun rewrite_thm mode prover mss = fconv_rule (rewrite_cterm mode prover mss);
    1.32