--- a/src/Pure/General/binding.ML Fri Dec 17 20:21:35 2010 +0100
+++ b/src/Pure/General/binding.ML Fri Dec 17 22:23:56 2010 +0100
@@ -30,6 +30,8 @@
val prefix: bool -> string -> binding -> binding
val conceal: binding -> binding
val str_of: binding -> string
+ val bad: binding -> string
+ val check: binding -> unit
end;
structure Binding: BINDING =
@@ -127,6 +129,16 @@
qualified_name_of binding
|> Markup.markup (Position.markup (pos_of binding) (Markup.binding (name_of binding)));
+
+(* check *)
+
+fun bad binding =
+ "Bad name binding: " ^ quote (str_of binding) ^ Position.str_of (pos_of binding);
+
+fun check binding =
+ if Symbol.is_ident (Symbol.explode (name_of binding)) then ()
+ else legacy_feature (bad binding);
+
end;
end;