--- a/src/Pure/Isar/named_target.ML Sun Apr 01 14:29:22 2012 +0200
+++ b/src/Pure/Isar/named_target.ML Sun Apr 01 15:23:43 2012 +0200
@@ -49,30 +49,10 @@
else error "Not in a named target (global theory, locale, class)";
-(* generic declarations *)
-
-fun locale_declaration locale syntax decl lthy =
- let
- val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
- val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
- in
- lthy
- |> Local_Theory.target (add locale locale_decl)
- end;
+(* consts in locale *)
-fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
- if target = "" then Generic_Target.standard_declaration decl lthy
- else
- lthy
- |> pervasive ? Generic_Target.background_declaration decl
- |> locale_declaration target syntax decl
- |> Context.proof_map (Morphism.form decl);
-
-
-(* consts in locales *)
-
-fun locale_const (ta as Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) =
- locale_declaration target true (fn phi =>
+fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) =
+ Generic_Target.locale_declaration target true (fn phi =>
let
val b' = Morphism.binding phi b;
val rhs' = Morphism.term phi rhs;
@@ -157,6 +137,18 @@
|> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
+(* declaration *)
+
+fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
+ if target = "" then Generic_Target.standard_declaration decl lthy
+ else
+ lthy
+ |> pervasive ? Generic_Target.background_declaration decl
+ |> Generic_Target.locale_declaration target syntax decl
+ |> (fn lthy' => lthy' |> Local_Theory.map_contexts (fn level => fn ctxt => ctxt |>
+ level > 0 ? Context.proof_map (Local_Theory.standard_form lthy' ctxt decl)));
+
+
(* pretty *)
fun pretty (Target {target, is_locale, is_class, ...}) ctxt =