--- a/src/Pure/net.ML Mon Mar 24 10:28:23 1997 +0100
+++ b/src/Pure/net.ML Tue Mar 25 10:41:44 1997 +0100
@@ -193,17 +193,16 @@
case net of
Leaf _ => nets
| Net{var,...} =>
- case (head_of t) of
- Var _ => if unif then net_skip (net,nets)
- else var::nets (*only matches Var in net*)
-(*If "unif" then a var instantiation in the abstraction could allow
- an eta-reduction, so regard the abstraction as a wildcard.*)
- | Abs(_,_,u) => (case u of
- f $ Bound 0 => if loose_bvar1(f,0) then var::nets
- else matching unif f (net,nets)
- | _ => if unif then net_skip (net,nets)
- else var::nets) (*only a Var can match*)
- | _ => rands t (net, var::nets) (*var could match also*)
+ let val etat = Pattern.eta_contract_atom t
+ in case (head_of etat) of
+ Var _ => if unif then net_skip (net,nets)
+ else var::nets (*only matches Var in net*)
+ (*If "unif" then a var instantiation in the abstraction could allow
+ an eta-reduction, so regard the abstraction as a wildcard.*)
+ | Abs _ => if unif then net_skip (net,nets)
+ else var::nets (*only a Var can match*)
+ | _ => rands etat (net, var::nets) (*var could match also*)
+ end
end;
fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l);