--- a/src/Pure/net.ML Thu Apr 29 15:35:40 1999 +0200
+++ b/src/Pure/net.ML Thu Apr 29 18:33:31 1999 +0200
@@ -195,16 +195,14 @@
case net of
Leaf _ => nets
| Net{var,...} =>
- let val etat = Pattern.eta_contract_atom t
- in case (head_of etat) of
+ 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 _ => 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
+ | _ => rands t (net, var::nets) (*var could match also*)
end;
fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l);