# HG changeset patch
# User wenzelm
# Date 1330171994 -3600
# Node ID 318b669fe660b31f4c3ec8b2e49946f05a845ed8
# Parent  b01b6977a5e862ff70d1da3459f88de413d0c341
standard Graph instances;

diff -r b01b6977a5e8 -r 318b669fe660 src/HOL/TPTP/atp_theory_export.ML
--- 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) =
diff -r b01b6977a5e8 -r 318b669fe660 src/Pure/General/graph.ML
--- 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);
diff -r b01b6977a5e8 -r 318b669fe660 src/Pure/General/graph.scala
--- 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)
 }