src/Pure/net.ML
changeset 2226 f3c6a22681b1
parent 1500 b2de3b3277b8
child 2672 85d7e800d754
--- a/src/Pure/net.ML	Tue Nov 26 16:07:17 1996 +0100
+++ b/src/Pure/net.ML	Tue Nov 26 16:11:18 1996 +0100
@@ -203,7 +203,7 @@
 	     | _ => rands t (net, var::nets)	(*var could match also*)
   end;
 
-val extract_leaves = flat o map (fn Leaf(xs) => xs);
+fun extract_leaves l = flat (map (fn Leaf(xs) => xs) l);
 
 (*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*)
 fun match_term net t =