diff -r f1f7964ed05c -r dfb214fa310b src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Mon Jan 21 14:47:55 2002 +0100
+++ b/src/Pure/pattern.ML	Mon Jan 21 14:48:11 2002 +0100
@@ -451,6 +451,6 @@
           end
       | rew2 _ = None
 
-  in if_none (timeap_msg "FIXME: rewrite_term" rew1 tm) tm end;
+  in if_none (rew1 tm) tm end;
 
 end;