--- a/src/Pure/Isar/named_target.ML Fri Oct 28 23:10:44 2011 +0200
+++ b/src/Pure/Isar/named_target.ML Fri Oct 28 23:16:50 2011 +0200
@@ -52,12 +52,13 @@
val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
in
lthy
- |> pervasive ? Generic_Target.theory_declaration decl
+ |> pervasive ? Generic_Target.theory_declaration syntax decl
|> Local_Theory.target (add locale locale_decl)
+ |> not syntax ? Context.proof_map (Morphism.form decl)
end;
fun target_declaration (Target {target, ...}) params =
- if target = "" then Generic_Target.theory_declaration
+ if target = "" then Generic_Target.theory_declaration (#syntax params)
else locale_declaration target params;