src/Pure/Isar/locale.ML
changeset 59859 f9d1442c70f3
parent 59498 50b60f501b05
child 59884 bbf49d7dfd6f
--- a/src/Pure/Isar/locale.ML	Mon Mar 30 22:34:59 2015 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Mar 31 00:11:54 2015 +0200
@@ -592,7 +592,7 @@
 
 fun add_decl loc decl =
   add_thmss loc ""
-    [((Binding.conceal Binding.empty,
+    [((Binding.concealed Binding.empty,
         [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
       [([Drule.dummy_thm], [])])];