src/Pure/net.ML
changeset 1500 b2de3b3277b8
parent 1460 5a6f2aabd538
child 2226 f3c6a22681b1
equal deleted inserted replaced
1499:01fdd1ea6324 1500:b2de3b3277b8
    29   val key_of_term: term -> key list
    29   val key_of_term: term -> key list
    30   val unify_term: 'a net -> term -> 'a list
    30   val unify_term: 'a net -> term -> 'a list
    31   end;
    31   end;
    32 
    32 
    33 
    33 
    34 functor NetFun () : NET = 
    34 structure Net : NET = 
    35 struct
    35 struct
    36 
    36 
    37 datatype key = CombK | VarK | AtomK of string;
    37 datatype key = CombK | VarK | AtomK of string;
    38 
    38 
    39 (*Bound variables*)
    39 (*Bound variables*)