src/Pure/net.ML
changeset 2792 6c17c5ec3d8b
parent 2672 85d7e800d754
child 2836 148829646a51
     1.1 --- a/src/Pure/net.ML	Tue Mar 11 17:20:59 1997 +0100
     1.2 +++ b/src/Pure/net.ML	Fri Mar 14 10:35:30 1997 +0100
     1.3 @@ -198,8 +198,11 @@
     1.4  			else var::nets	   	(*only matches Var in net*)
     1.5  (*If "unif" then a var instantiation in the abstraction could allow
     1.6    an eta-reduction, so regard the abstraction as a wildcard.*)
     1.7 -	     | Abs _ => if unif then net_skip (net,nets)
     1.8 -			else var::nets		(*only a Var can match*)
     1.9 +	     | Abs(_,_,u) => (case u of
    1.10 +                   f $ Bound 0 => if loose_bvar1(f,0) then var::nets
    1.11 +                                  else matching unif f (net,nets)
    1.12 +                 | _ => if unif then net_skip (net,nets)
    1.13 +			else var::nets)		(*only a Var can match*)
    1.14  	     | _ => rands t (net, var::nets)	(*var could match also*)
    1.15    end;
    1.16