1.1 --- a/src/Pure/Isar/named_target.ML	Fri Oct 28 23:10:44 2011 +0200
     1.2 +++ b/src/Pure/Isar/named_target.ML	Fri Oct 28 23:16:50 2011 +0200
     1.3 @@ -52,12 +52,13 @@
     1.4      val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
     1.5    in
     1.6      lthy
     1.7 -    |> pervasive ? Generic_Target.theory_declaration decl
     1.8 +    |> pervasive ? Generic_Target.theory_declaration syntax decl
     1.9      |> Local_Theory.target (add locale locale_decl)
    1.10 +    |> not syntax ? Context.proof_map (Morphism.form decl)
    1.11    end;
    1.12  
    1.13  fun target_declaration (Target {target, ...}) params =
    1.14 -  if target = "" then Generic_Target.theory_declaration
    1.15 +  if target = "" then Generic_Target.theory_declaration (#syntax params)
    1.16    else locale_declaration target params;
    1.17  
    1.18