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