--- a/src/Pure/Isar/named_target.ML Sun Jun 08 23:30:50 2014 +0200
+++ b/src/Pure/Isar/named_target.ML Sun Jun 08 23:30:51 2014 +0200
@@ -105,7 +105,7 @@
fun declaration (Target {target, is_locale, ...}) {syntax, pervasive} decl =
if is_locale then
pervasive ? Generic_Target.background_declaration decl
- #> Generic_Target.locale_declaration target syntax decl
+ #> Generic_Target.locale_target_declaration target syntax decl
#> Generic_Target.standard_declaration (fn (_, other) => other <> 0) decl
else Generic_Target.theory_declaration decl;