# HG changeset patch
# User wenzelm
# Date 1002202831 -7200
# Node ID abd396ca7ef9bc98de65fcf0d51bfb3a796ebbc0
# Parent  f2268239b93f6f1f8256ff328ab5f71192e2c62f
removed hol_rewrite_cterm (use full_rewrite_cterm from Pure);

diff -r f2268239b93f -r abd396ca7ef9 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Oct 04 15:40:05 2001 +0200
+++ b/src/HOL/simpdata.ML	Thu Oct 04 15:40:31 2001 +0200
@@ -390,8 +390,6 @@
      addsplits [split_if];
 
 fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
-fun hol_rewrite_cterm rews =
-  #2 o Thm.dest_comb o #prop o Thm.crep_thm o Simplifier.full_rewrite (HOL_basic_ss addsimps rews);
 
 
 (*Simplifies x assuming c and y assuming ~c*)