# HG changeset patch
# User wenzelm
# Date 869649074 -7200
# Node ID 7db9a44dfa0629645328ff7cbe9688e512ad01b0
# Parent  7a176613e5d5a1f22fd384134e6328c287c5909f
fixed polymorphic val;

diff -r 7a176613e5d5 -r 7db9a44dfa06 src/Pure/net.ML
--- a/src/Pure/net.ML	Wed Jul 23 11:07:36 1997 +0200
+++ b/src/Pure/net.ML	Wed Jul 23 11:11:14 1997 +0200
@@ -221,13 +221,12 @@
 (** dest **)
 
 fun cons_fst x (xs, y) = (x :: xs, y);
-val cons_fsts = map o cons_fst;
 
 fun dest (Leaf xs) = map (pair []) xs
   | dest (Net {comb, var, alist}) =
-      cons_fsts CombK (dest comb) @
-      cons_fsts VarK (dest var) @
-      flat (map (fn (a, net) => cons_fsts (AtomK a) (dest net)) alist);
+      map (cons_fst CombK) (dest comb) @
+      map (cons_fst VarK) (dest var) @
+      flat (map (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) alist);
 
 
 (** merge **)