tuned;
authorwenzelm
Sun Oct 14 20:08:11 2001 +0200 (2001-10-14)
changeset 117608e906f051fbc
parent 11759 56c80e542e44
child 11761 183435fd45f2
tuned;
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Sun Oct 14 20:07:32 2001 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Sun Oct 14 20:08:11 2001 +0200
     1.3 @@ -44,7 +44,7 @@
     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_cterm_aux: (meta_simpset -> thm -> thm option) -> thm list -> cterm -> cterm
     1.8 +  val full_rewrite_aux: (meta_simpset -> thm -> thm option) -> thm list -> cterm -> thm
     1.9    val rewrite_rule_aux  : (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    1.10    val rewrite_thm       : bool * bool * bool
    1.11                            -> (meta_simpset -> thm -> thm option)
    1.12 @@ -949,16 +949,14 @@
    1.13  (*Use a conversion to transform a theorem*)
    1.14  fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
    1.15  
    1.16 -(*Rewrite a cterm (yielding again a cterm instead of a theorem)*)
    1.17 -fun full_rewrite_cterm_aux _ [] = (fn ct => ct)
    1.18 -  | full_rewrite_cterm_aux prover thms =
    1.19 -      #2 o Thm.dest_comb o #prop o Thm.crep_thm o
    1.20 -        rewrite_cterm (true, false, false) prover (mss_of thms);
    1.21 +(*Rewrite a cterm*)
    1.22 +fun full_rewrite_aux _ [] = (fn ct => Thm.reflexive ct)
    1.23 +  | full_rewrite_aux prover thms = rewrite_cterm (true, false, false) prover (mss_of thms);
    1.24  
    1.25  (*Rewrite a theorem*)
    1.26  fun rewrite_rule_aux _ [] = (fn th => th)
    1.27    | rewrite_rule_aux prover thms =
    1.28 -      fconv_rule (rewrite_cterm (true,false,false) prover (mss_of thms));
    1.29 +      fconv_rule (rewrite_cterm (true, 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