# HG changeset patch
# User wenzelm
# Date 1330004798 -3600
# Node ID 0a881b8c066e00db395561f1a0b32a6f41e6675d
# Parent  669601fa1a629adebb1c93fdcd4b11d716787ae2
removed dead code;

diff -r 669601fa1a62 -r 0a881b8c066e 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;