--- a/src/Pure/General/binding.ML Wed Sep 16 13:43:15 2009 +0200
+++ b/src/Pure/General/binding.ML Wed Sep 16 21:14:08 2009 +0200
@@ -30,18 +30,19 @@
val str_of: binding -> string
end;
-structure Binding:> BINDING =
+structure Binding: BINDING =
struct
(** representation **)
(* datatype *)
-datatype binding = Binding of
+abstype binding = Binding of
{prefix: (string * bool) list, (*system prefix*)
qualifier: (string * bool) list, (*user qualifier*)
name: bstring, (*base name*)
- pos: Position.T}; (*source position*)
+ pos: Position.T} (*source position*)
+with
fun make_binding (prefix, qualifier, name, pos) =
Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos};
@@ -109,6 +110,7 @@
in Markup.markup (Markup.properties props (Markup.binding (name_of binding))) text end;
end;
+end;
type binding = Binding.binding;