Removed timing function.
authorberghofe
Mon, 21 Jan 2002 14:48:11 +0100
changeset 12826 dfb214fa310b
parent 12825 f1f7964ed05c
child 12827 05c13f5a515d
Removed timing function.
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;