--- a/src/Pure/Isar/generic_target.ML Mon Apr 02 20:50:41 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML Mon Apr 02 21:49:27 2012 +0200
@@ -33,6 +33,7 @@
(Attrib.binding * (thm list * Args.src list) list) list ->
local_theory -> local_theory
val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
+ val theory_declaration: declaration -> local_theory -> local_theory
end
structure Generic_Target: GENERIC_TARGET =
@@ -209,10 +210,9 @@
(Proof_Context.init_global (Proof_Context.theory_of lthy)) decl;
in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end;
-fun standard_declaration decl =
- background_declaration decl #>
- (fn lthy => Local_Theory.map_contexts (fn _ => fn ctxt =>
- Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt) lthy);
+fun standard_declaration decl lthy =
+ Local_Theory.map_contexts (fn _ => fn ctxt =>
+ Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt) lthy;
fun locale_declaration locale syntax decl lthy = lthy
|> Local_Theory.target (fn ctxt => ctxt |>
@@ -247,4 +247,7 @@
(Sign.add_abbrev (#1 prmode) (b, t) #->
(fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
+fun theory_declaration decl =
+ background_declaration decl #> standard_declaration decl;
+
end;