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], [])])];