# HG changeset patch
# User wenzelm
# Date 1310505742 -7200
# Node ID 9bd8d4addd6e29dd056a711740935deb6ae809cd
# Parent  321ebd0518974e7c5fc35aa092139af11eb100c7
more thorough Variable.check_name: Binding.check for logical entities within the term language;

diff -r 321ebd051897 -r 9bd8d4addd6e src/Pure/variable.ML
--- a/src/Pure/variable.ML	Tue Jul 12 23:20:34 2011 +0200
+++ b/src/Pure/variable.ML	Tue Jul 12 23:22:22 2011 +0200
@@ -165,7 +165,8 @@
 
 val is_declared = Name.is_declared o names_of;
 
-val check_name = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
+val check_name =
+  Long_Name.base_name o Name_Space.full_name Name_Space.default_naming o tap Binding.check;