# HG changeset patch
# User paulson
# Date 859282904 -3600
# Node ID 148829646a51a22f3b334fb2d053ebdad324f8b3
# Parent  c07d6bc56cc297762068582bc7be6ba5e8942416
Toby's better treatment of eta-contraction

diff -r c07d6bc56cc2 -r 148829646a51 src/Pure/net.ML
--- a/src/Pure/net.ML	Mon Mar 24 10:28:23 1997 +0100
+++ b/src/Pure/net.ML	Tue Mar 25 10:41:44 1997 +0100
@@ -193,17 +193,16 @@
      case net of
 	 Leaf _ => nets
        | Net{var,...} =>
-	   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(_,_,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*)
+	     let val etat = Pattern.eta_contract_atom t
+	     in case (head_of etat) 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*)
+	       | _ => rands etat (net, var::nets)  (*var could match also*)
+	     end
   end;
 
 fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l);