src/Pure/net.ML
changeset 6539 2e7d2fba9f6c
parent 3560 7db9a44dfa06
child 7943 e31a3c0c2c1e
     1.1 --- a/src/Pure/net.ML	Thu Apr 29 15:35:40 1999 +0200
     1.2 +++ b/src/Pure/net.ML	Thu Apr 29 18:33:31 1999 +0200
     1.3 @@ -195,16 +195,14 @@
     1.4       case net of
     1.5  	 Leaf _ => nets
     1.6         | Net{var,...} =>
     1.7 -	     let val etat = Pattern.eta_contract_atom t
     1.8 -	     in case (head_of etat) of
     1.9 +	     case head_of t of
    1.10  		 Var _ => if unif then net_skip (net,nets)
    1.11  			  else var::nets	   (*only matches Var in net*)
    1.12    (*If "unif" then a var instantiation in the abstraction could allow
    1.13      an eta-reduction, so regard the abstraction as a wildcard.*)
    1.14  	       | Abs _ => if unif then net_skip (net,nets)
    1.15  			  else var::nets	   (*only a Var can match*)
    1.16 -	       | _ => rands etat (net, var::nets)  (*var could match also*)
    1.17 -	     end
    1.18 +	       | _ => rands t (net, var::nets)  (*var could match also*)
    1.19    end;
    1.20  
    1.21  fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l);