more thorough Variable.check_name: Binding.check for logical entities within the term language;
authorwenzelm
Tue, 12 Jul 2011 23:22:22 +0200
changeset 43790 9bd8d4addd6e
parent 43789 321ebd051897
child 43791 5e9a1d71f94d
child 43799 a72661ba7239
child 43801 097732301fc0
more thorough Variable.check_name: Binding.check for logical entities within the term language;
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;