src/Pure/net.ML

--- a/src/Pure/net.ML	Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/net.ML	Fri Feb 21 15:31:47 1997 +0100
@@ -203,7 +203,7 @@
 	     | _ => rands t (net, var::nets)	(*var could match also*)
   end;
 
-fun extract_leaves l = flat (map (fn Leaf(xs) => xs) l);
+fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l);
 
 (*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*)
 fun match_term net t =