# HG changeset patch
# User wenzelm
# Date 1120672842 -7200
# Node ID ff304c52bf86213766270fec56565d662aa8f933
# Parent  24c5c94aa967e23ece2f644c70a4b42c2dcadd1c
removed timers;

diff -r 24c5c94aa967 -r ff304c52bf86 src/Pure/net.ML
--- a/src/Pure/net.ML	Wed Jul 06 20:00:41 2005 +0200
+++ b/src/Pure/net.ML	Wed Jul 06 20:00:42 2005 +0200
@@ -14,8 +14,6 @@
 only wildcards in patterns.  Requires operands to be beta-eta-normal.
 *)
 
-val time_string_of_bound = time_init ();
-
 signature NET =
   sig
   type key
@@ -41,7 +39,6 @@
 
 (*Bound variables*)
 fun string_of_bound i = "*B*" ^ chr (i div 256) ^ chr (i mod 256);
-val string_of_bound = time time_string_of_bound string_of_bound;
 
 (*Keys are preorder lists of symbols -- Combinations, Vars, Atoms.
   Any term whose head is a Var is regarded entirely as a Var.