Removed timing function.
--- 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;