--- a/src/Tools/Code/code_symbol.ML Sat Jan 18 21:03:54 2014 +0100
+++ b/src/Tools/Code/code_symbol.ML Sun Jan 19 11:05:37 2014 +0100
@@ -11,6 +11,7 @@
Constant of 'a | Type_Constructor of 'b | Type_Class of 'c |
Class_Relation of 'd | Class_Instance of 'e | Module of 'f
type symbol = (string, string, class, class * class, string * class, string) attr
+ structure Table: TABLE;
structure Graph: GRAPH;
val default_name: Proof.context -> symbol -> string * string
val quote_symbol: Proof.context -> symbol -> string
@@ -74,6 +75,7 @@
| symbol_ord (_, Class_Instance _) = LESS
| symbol_ord (Module name1, Module name2) = fast_string_ord (name1, name2);
+structure Table = Table(type key = symbol val ord = symbol_ord);
structure Graph = Graph(type key = symbol val ord = symbol_ord);
local