removed dead code;
authorwenzelm
Thu, 23 Feb 2012 14:46:38 +0100
changeset 46612 0a881b8c066e
parent 46611 669601fa1a62
child 46613 74331911375d
removed dead code;
src/Pure/General/graph.ML
--- 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;