diff -r 0246a314b57d -r 40c352510065 src/Pure/net.ML
--- a/src/Pure/net.ML	Thu Jun 24 11:08:21 2010 +0200
+++ b/src/Pure/net.ML	Thu Jun 24 11:28:34 2010 +0200
@@ -17,6 +17,7 @@
 sig
   type key
   val key_of_term: term -> key list
+  val encode_type: typ -> term
   type 'a net
   val empty: 'a net
   exception INSERT
@@ -62,6 +63,11 @@
 (*convert a term to a list of keys*)
 fun key_of_term t = add_key_of_terms (t, []);
 
+(*encode_type -- for indexing purposes*)
+fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts)
+  | encode_type (TFree (a, _)) = Free (a, dummyT)
+  | encode_type (TVar (a, _)) = Var (a, dummyT);
+
 
 (*Trees indexed by key lists: each arc is labelled by a key.
   Each node contains a list of items, and arcs to children.