# HG changeset patch
# User haftmann
# Date 1390125937 -3600
# Node ID 29e1657b73891675d7320b3319c7709c8db8082d
# Parent  368ee97e03ce5033fa1cf2d2de9e77989cc073b7
table for code symbols

diff -r 368ee97e03ce -r 29e1657b7389 src/Tools/Code/code_symbol.ML
--- 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