standard Graph instances;

--- a/src/HOL/TPTP/atp_theory_export.ML	Sat Feb 25 13:00:32 2012 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML	Sat Feb 25 13:13:14 2012 +0100
@@ -143,8 +143,6 @@
                  [(factsN, [Formula (ident, Conjecture, phi, NONE, [])])])
   | is_problem_line_tautology _ _ _ = false
 
-structure String_Graph = Graph(type key = string val ord = string_ord);
-
 fun order_facts ord = sort (ord o pairself ident_of_problem_line)
 fun order_problem_facts _ [] = []
   | order_problem_facts ord ((heading, lines) :: problem) =

--- a/src/Pure/General/graph.ML	Sat Feb 25 13:00:32 2012 +0100
+++ b/src/Pure/General/graph.ML	Sat Feb 25 13:13:14 2012 +0100
@@ -319,4 +319,5 @@
 end;
 
 structure Graph = Graph(type key = string val ord = fast_string_ord);
+structure String_Graph = Graph(type key = string val ord = string_ord);
 structure Int_Graph = Graph(type key = int val ord = int_ord);

--- a/src/Pure/General/graph.scala	Sat Feb 25 13:00:32 2012 +0100
+++ b/src/Pure/General/graph.scala	Sat Feb 25 13:13:14 2012 +0100
@@ -20,6 +20,10 @@
 
   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
     new Graph[Key, A](SortedMap.empty(ord))
+
+  def string[A]: Graph[String, A] = empty(Ordering.String)
+  def int[A]: Graph[Int, A] = empty(Ordering.Int)
+  def long[A]: Graph[Long, A] = empty(Ordering.Long)
 }