src/Tools/induct.ML
changeset 37523 40c352510065
parent 36960 01594f816e3a
child 37524 a9e38cdbfe07
     1.1 --- a/src/Tools/induct.ML	Thu Jun 24 11:08:21 2010 +0200
     1.2 +++ b/src/Tools/induct.ML	Thu Jun 24 11:28:34 2010 +0200
     1.3 @@ -85,24 +85,14 @@
     1.4  functor Induct(Data: INDUCT_DATA): INDUCT =
     1.5  struct
     1.6  
     1.7 -
     1.8 -(** misc utils **)
     1.9 -
    1.10 -(* encode_type -- for indexing purposes *)
    1.11 -
    1.12 -fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts)
    1.13 -  | encode_type (TFree (a, _)) = Free (a, dummyT)
    1.14 -  | encode_type (TVar (a, _)) = Var (a, dummyT);
    1.15 -
    1.16 -
    1.17 -(* variables -- ordered left-to-right, preferring right *)
    1.18 +(** variables -- ordered left-to-right, preferring right **)
    1.19  
    1.20  fun vars_of tm =
    1.21    rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []));
    1.22  
    1.23  local
    1.24  
    1.25 -val mk_var = encode_type o #2 o Term.dest_Var;
    1.26 +val mk_var = Net.encode_type o #2 o Term.dest_Var;
    1.27  
    1.28  fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
    1.29    raise THM ("No variables in conclusion of rule", 0, [thm]);
    1.30 @@ -272,11 +262,11 @@
    1.31  fun find_rules which how ctxt x =
    1.32    map snd (Item_Net.retrieve (which (get_local ctxt)) (how x));
    1.33  
    1.34 -val find_casesT = find_rules (#1 o #1) encode_type;
    1.35 +val find_casesT = find_rules (#1 o #1) Net.encode_type;
    1.36  val find_casesP = find_rules (#2 o #1) I;
    1.37 -val find_inductT = find_rules (#1 o #2) encode_type;
    1.38 +val find_inductT = find_rules (#1 o #2) Net.encode_type;
    1.39  val find_inductP = find_rules (#2 o #2) I;
    1.40 -val find_coinductT = find_rules (#1 o #3) encode_type;
    1.41 +val find_coinductT = find_rules (#1 o #3) Net.encode_type;
    1.42  val find_coinductP = find_rules (#2 o #3) I;
    1.43  
    1.44