# HG changeset patch
# User wenzelm
# Date 1277371714 -7200
# Node ID 40c352510065b102295ab5ddf92f01ea03376d00
# Parent  0246a314b57d9f4ecd20615aa1f5d96f10e0e2e4
Net.encode_type;

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.
diff -r 0246a314b57d -r 40c352510065 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Thu Jun 24 11:08:21 2010 +0200
+++ b/src/Tools/induct.ML	Thu Jun 24 11:28:34 2010 +0200
@@ -85,24 +85,14 @@
 functor Induct(Data: INDUCT_DATA): INDUCT =
 struct
 
-
-(** misc utils **)
-
-(* 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);
-
-
-(* variables -- ordered left-to-right, preferring right *)
+(** variables -- ordered left-to-right, preferring right **)
 
 fun vars_of tm =
   rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []));
 
 local
 
-val mk_var = encode_type o #2 o Term.dest_Var;
+val mk_var = Net.encode_type o #2 o Term.dest_Var;
 
 fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
   raise THM ("No variables in conclusion of rule", 0, [thm]);
@@ -272,11 +262,11 @@
 fun find_rules which how ctxt x =
   map snd (Item_Net.retrieve (which (get_local ctxt)) (how x));
 
-val find_casesT = find_rules (#1 o #1) encode_type;
+val find_casesT = find_rules (#1 o #1) Net.encode_type;
 val find_casesP = find_rules (#2 o #1) I;
-val find_inductT = find_rules (#1 o #2) encode_type;
+val find_inductT = find_rules (#1 o #2) Net.encode_type;
 val find_inductP = find_rules (#2 o #2) I;
-val find_coinductT = find_rules (#1 o #3) encode_type;
+val find_coinductT = find_rules (#1 o #3) Net.encode_type;
 val find_coinductP = find_rules (#2 o #3) I;