# HG changeset patch
# User wenzelm
# Date 1187635441 -7200
# Node ID 52a14669f9e9bd7e49de99e7dab08d9804b9e2b1
# Parent  a0da34cc081ce007a69135b360156dc5b7b1078f
tuned signature;

diff -r a0da34cc081c -r 52a14669f9e9 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Aug 20 20:44:00 2007 +0200
+++ b/src/Pure/General/name_space.ML	Mon Aug 20 20:44:01 2007 +0200
@@ -51,7 +51,7 @@
   val sticky_prefix: string -> naming -> naming
   val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
     naming -> naming
-  type 'a table (*= T * 'a Symtab.table*)
+  type 'a table = T * 'a Symtab.table
   val empty_table: 'a table
   val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
   val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table