# HG changeset patch
# User wenzelm
# Date 1441201752 -7200
# Node ID 56ce4474edbc2405034ee38fcac6c7c7ab94c1ea
# Parent  3bccde9cbb9db63bf892e0e9d793c97dc6905746
clarified vacuous binding;

diff -r 3bccde9cbb9d -r 56ce4474edbc src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Sep 02 13:26:29 2015 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Sep 02 15:49:12 2015 +0200
@@ -608,8 +608,7 @@
 
 fun add_decl loc decl =
   add_thmss loc ""
-    [((Binding.concealed Binding.empty,
-        [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
+    [((Binding.empty, [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
       [([Drule.dummy_thm], [])])];
 
 in