src/Pure/net.ML

 	   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 _ => 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;
 
 fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l);