author | wenzelm |
Thu, 23 Feb 2012 14:46:38 +0100 | |
changeset 46612 | 0a881b8c066e |
parent 46611 | 669601fa1a62 |
child 46613 | 74331911375d |
--- a/src/Pure/General/graph.ML Thu Feb 23 14:17:51 2012 +0100 +++ b/src/Pure/General/graph.ML Thu Feb 23 14:46:38 2012 +0100 @@ -91,7 +91,6 @@ fun fold f (Keys tab) = Table.fold (f o #1) tab; fun fold_rev f (Keys tab) = Table.fold_rev (f o #1) tab; -fun make xs = Basics.fold insert xs empty; fun dest keys = fold_rev cons keys []; fun filter P keys = fold (fn x => P x ? insert x) keys empty;