src/Pure/net.ML
changeset 2226 f3c6a22681b1
parent 1500 b2de3b3277b8
child 2672 85d7e800d754
     1.1 --- a/src/Pure/net.ML	Tue Nov 26 16:07:17 1996 +0100
     1.2 +++ b/src/Pure/net.ML	Tue Nov 26 16:11:18 1996 +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 -val extract_leaves = flat o map (fn Leaf(xs) => xs);
     1.8 +fun extract_leaves l = flat (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 =