diff -r 5415c6ad0028 -r 4f43430f226e src/Pure/net.ML
--- a/src/Pure/net.ML	Fri Jan 14 12:42:49 1994 +0100
+++ b/src/Pure/net.ML	Tue Jan 18 07:53:35 1994 +0100
@@ -10,8 +10,8 @@
     Artificial Intelligence Programming.
     (Lawrence Erlbaum Associates, 1980).  [Chapter 14]
 
-match_term no longer treats abstractions as wildcards but as the constant
-*Abs*.  Requires operands to be beta-eta-normal.
+match_term no longer treats abstractions as wildcards; instead they match 
+only wildcards in patterns.  Requires operands to be beta-eta-normal.
 *)
 
 signature NET = 
@@ -39,10 +39,10 @@
 (*Bound variables*)
 fun string_of_bound i = "*B*" ^ chr i;
 
-(*Keys are preorder lists of symbols -- constants, Vars, bound vars, ...
+(*Keys are preorder lists of symbols -- Combinations, Vars, Atoms.
   Any term whose head is a Var is regarded entirely as a Var.
-  Abstractions are also regarded as Vars.  This covers eta-conversion
-    and "near" eta-conversions such as %x.P(?f(x)).
+  Abstractions are also regarded as Vars;  this covers eta-conversion
+    and "near" eta-conversions such as %x.?P(?f(x)).
 *)
 fun add_key_of_terms (t, cs) = 
   let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs))
@@ -51,7 +51,7 @@
 	| rands (Bound i,  cs)   = AtomK (string_of_bound i) :: cs
   in case (head_of t) of
       Var _ => VarK :: cs
-    | Abs (_,_,t) => VarK :: cs
+    | Abs _ => VarK :: cs
     | _     => rands(t,cs)
   end;
 
@@ -188,19 +188,19 @@
 	      | Const(c,_) => look1 (alist, c) nets
 	      | Free(c,_)  => look1 (alist, c) nets
 	      | Bound i    => look1 (alist, string_of_bound i) nets
-	      | Abs _      => look1 (alist, "*Abs*") nets
+	      | _      	   => nets
   in 
      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*)
+	       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) => if unif then net_skip (net,nets)
-                             else rands t (net, var::nets)
-	     | _ => rands t (net, var::nets)	   (*var could match also*)
+	     | Abs _ => 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;
 
 val extract_leaves = flat o map (fn Leaf(xs) => xs);