author | wenzelm |
Thu, 04 Oct 2001 16:07:20 +0200 | |
changeset 11689 | 38788d98504f |
parent 11688 | 56833637db2a |
child 11690 | cb64368fb405 |
--- a/src/Pure/meta_simplifier.ML Thu Oct 04 15:43:17 2001 +0200 +++ b/src/Pure/meta_simplifier.ML Thu Oct 04 16:07:20 2001 +0200 @@ -909,8 +909,6 @@ prover: how to solve premises in conditional rewrites and congruences *) -(* FIXME: check that #bounds(mss) does not "occur" in ct already *) - fun rewrite_cterm mode prover mss ct = let val {sign, t, maxidx, ...} = rep_cterm ct val Mss{depth, ...} = mss