# HG changeset patch
# User wenzelm
# Date 1310681027 -7200
# Node ID 1183951365de3b2fab73d8e8475d56f64d315c3e
# Parent  136ac1de4cbc63137b190095dbb39525d957e7fa
do not check vacous bindings, which routinely occur in locale expressions and long theorem statements etc.;

diff -r 136ac1de4cbc -r 1183951365de src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Thu Jul 14 23:05:25 2011 +0200
+++ b/src/Pure/Isar/element.ML	Fri Jul 15 00:03:47 2011 +0200
@@ -526,7 +526,7 @@
 
 fun activate raw_elem ctxt =
   let val elem = raw_elem |> map_ctxt
-   {binding = tap Variable.check_name,
+   {binding = tap (fn b => if Binding.is_empty b then "" else Variable.check_name b),
     typ = I,
     term = I,
     pattern = I,