--- a/src/Pure/net.ML Tue Mar 11 17:20:59 1997 +0100
+++ b/src/Pure/net.ML Fri Mar 14 10:35:30 1997 +0100
@@ -198,8 +198,11 @@
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*)
+ | 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*)
end;