src/Pure/General/binding.ML

--- a/src/Pure/General/binding.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/General/binding.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -6,6 +6,7 @@
 
 signature BASIC_BINDING =
 sig
+  type binding
   val long_names: bool ref
   val short_names: bool ref
   val unique_names: bool ref
@@ -92,6 +93,8 @@
     else space_implode "." (map mk_prefix prefix) ^ ":" ^ name
   end;
 
+type binding = T;
+
 end;
 
 structure Basic_Binding : BASIC_BINDING = Binding;