# HG changeset patch
# User wenzelm
# Date 1002204440 -7200
# Node ID 38788d98504f0a09bac472ef7e95c8b99921bd94
# Parent  56833637db2af69870f0d7dfe419aada0a9653fa
removed obsolete comment;

diff -r 56833637db2a -r 38788d98504f src/Pure/meta_simplifier.ML
--- 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