src/Pure/consts.ML

--- a/src/Pure/consts.ML	Fri Dec 17 20:21:35 2010 +0100
+++ b/src/Pure/consts.ML	Fri Dec 17 22:23:56 2010 +0100
@@ -235,6 +235,7 @@
   map_consts (fn (decls, constraints, rev_abbrevs) =>
     let
       val decl = {T = declT, typargs = typargs_of declT};
+      val _ = Binding.check b;
       val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE));
     in (decls', constraints, rev_abbrevs) end);
 
@@ -287,6 +288,7 @@
       let
         val decl = {T = T, typargs = typargs_of T};
         val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
+        val _ = Binding.check b;
         val (_, decls') = decls
           |> Name_Space.define true naming (b, (decl, SOME abbr));
         val rev_abbrevs' = rev_abbrevs