removed hol_rewrite_cterm (use full_rewrite_cterm from Pure);
authorwenzelm
Thu Oct 04 15:40:31 2001 +0200 (2001-10-04)
changeset 11684abd396ca7ef9
parent 11683 f2268239b93f
child 11685 c786d9ce558e
removed hol_rewrite_cterm (use full_rewrite_cterm from Pure);
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Thu Oct 04 15:40:05 2001 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Thu Oct 04 15:40:31 2001 +0200
     1.3 @@ -390,8 +390,6 @@
     1.4       addsplits [split_if];
     1.5  
     1.6  fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
     1.7 -fun hol_rewrite_cterm rews =
     1.8 -  #2 o Thm.dest_comb o #prop o Thm.crep_thm o Simplifier.full_rewrite (HOL_basic_ss addsimps rews);
     1.9  
    1.10  
    1.11  (*Simplifies x assuming c and y assuming ~c*)