table for code symbols
authorhaftmann
Sun, 19 Jan 2014 11:05:37 +0100
changeset 55042 29e1657b7389
parent 55041 368ee97e03ce
child 55043 acefda71629b
table for code symbols
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