--- 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.