1.1 --- a/src/Pure/net.ML	Mon Mar 24 10:28:23 1997 +0100
     1.2 +++ b/src/Pure/net.ML	Tue Mar 25 10:41:44 1997 +0100
     1.3 @@ -193,17 +193,16 @@
     1.4       case net of
     1.5  	 Leaf _ => nets
     1.6         | Net{var,...} =>
     1.7 -	   case (head_of t) of
     1.8 -	       Var _ => if unif then net_skip (net,nets)
     1.9 -			else var::nets	   	(*only matches Var in net*)
    1.10 -(*If "unif" then a var instantiation in the abstraction could allow
    1.11 -  an eta-reduction, so regard the abstraction as a wildcard.*)
    1.12 -	     | Abs(_,_,u) => (case u of
    1.13 -                   f $ Bound 0 => if loose_bvar1(f,0) then var::nets
    1.14 -                                  else matching unif f (net,nets)
    1.15 -                 | _ => if unif then net_skip (net,nets)
    1.16 -			else var::nets)		(*only a Var can match*)
    1.17 -	     | _ => rands t (net, var::nets)	(*var could match also*)
    1.18 +	     let val etat = Pattern.eta_contract_atom t
    1.19 +	     in case (head_of etat) of
    1.20 +		 Var _ => if unif then net_skip (net,nets)
    1.21 +			  else var::nets	   (*only matches Var in net*)
    1.22 +  (*If "unif" then a var instantiation in the abstraction could allow
    1.23 +    an eta-reduction, so regard the abstraction as a wildcard.*)
    1.24 +	       | Abs _ => if unif then net_skip (net,nets)
    1.25 +			  else var::nets	   (*only a Var can match*)
    1.26 +	       | _ => rands etat (net, var::nets)  (*var could match also*)
    1.27 +	     end
    1.28    end;
    1.29  
    1.30  fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l);