src/Pure/net.ML
changeset 2672 85d7e800d754
parent 2226 f3c6a22681b1
child 2792 6c17c5ec3d8b
     1.1 --- a/src/Pure/net.ML	Fri Feb 21 15:30:41 1997 +0100
     1.2 +++ b/src/Pure/net.ML	Fri Feb 21 15:31:47 1997 +0100
     1.3 @@ -203,7 +203,7 @@
     1.4  	     | _ => rands t (net, var::nets)	(*var could match also*)
     1.5    end;
     1.6  
     1.7 -fun extract_leaves l = flat (map (fn Leaf(xs) => xs) l);
     1.8 +fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l);
     1.9  
    1.10  (*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*)
    1.11  fun match_term net t =