1.1 --- a/src/Pure/Isar/named_target.ML	Sat Oct 29 12:55:34 2011 +0200
     1.2 +++ b/src/Pure/Isar/named_target.ML	Sat Oct 29 12:57:43 2011 +0200
     1.3 @@ -54,7 +54,6 @@
     1.4      lthy
     1.5      |> pervasive ? Generic_Target.theory_declaration syntax decl
     1.6      |> Local_Theory.target (add locale locale_decl)
     1.7 -    |> not syntax ? Context.proof_map (Morphism.form decl)
     1.8    end;
     1.9  
    1.10  fun target_declaration (Target {target, ...}) params =