1.1 --- a/src/Pure/Isar/named_target.ML	Sun Oct 30 22:20:45 2011 +0100
     1.2 +++ b/src/Pure/Isar/named_target.ML	Sun Oct 30 22:35:18 2011 +0100
     1.3 @@ -46,19 +46,21 @@
     1.4  
     1.5  (* generic declarations *)
     1.6  
     1.7 -fun locale_declaration locale {syntax, pervasive} decl lthy =
     1.8 +fun locale_declaration locale syntax decl lthy =
     1.9    let
    1.10      val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
    1.11      val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
    1.12    in
    1.13      lthy
    1.14 -    |> pervasive ? Generic_Target.theory_declaration decl
    1.15      |> Local_Theory.target (add locale locale_decl)
    1.16    end;
    1.17  
    1.18 -fun target_declaration (Target {target, ...}) params =
    1.19 -  if target = "" then Generic_Target.theory_declaration
    1.20 -  else locale_declaration target params;
    1.21 +fun target_declaration (Target {target, ...}) {syntax, pervasive} decl =
    1.22 +  if target = "" then Generic_Target.theory_declaration decl
    1.23 +  else
    1.24 +    locale_declaration target syntax decl
    1.25 +    #> pervasive ? Generic_Target.theory_declaration decl
    1.26 +    #> not pervasive ? Context.proof_map (Morphism.form decl);
    1.27  
    1.28  
    1.29  (* consts in locales *)
    1.30 @@ -89,7 +91,7 @@
    1.31    end;
    1.32  
    1.33  fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
    1.34 -  locale_declaration target {syntax = true, pervasive = false} (locale_const ta prmode arg);
    1.35 +  locale_declaration target true (locale_const ta prmode arg);
    1.36  
    1.37  
    1.38  (* define *)