src/Pure/pattern.ML
changeset 12826 dfb214fa310b
parent 12817 fcbb6ad5c790
child 12980 8f717cbd4e44
--- 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;