# HG changeset patch
# User wenzelm
# Date 1333396167 -7200
# Node ID 4bab649dedf0762c761ffcd6cac75aac144d56ce
# Parent  daeaf4824e9a4292a950bc5b700f501ffb6ded8d
clarified standard_declaration vs. theory_declaration;

diff -r daeaf4824e9a -r 4bab649dedf0 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Apr 02 20:50:41 2012 +0200
+++ b/src/Pure/Isar/class.ML	Mon Apr 02 21:49:27 2012 +0200
@@ -556,7 +556,7 @@
         abbrev = Generic_Target.abbrev
           (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
             Generic_Target.theory_abbrev prmode ((b, mx), t)),
-        declaration = K Generic_Target.standard_declaration,
+        declaration = K Generic_Target.theory_declaration,
         pretty = pretty,
         exit = Local_Theory.target_of o conclude}
   end;
diff -r daeaf4824e9a -r 4bab649dedf0 src/Pure/Isar/generic_target.ML
--- 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;
diff -r daeaf4824e9a -r 4bab649dedf0 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Mon Apr 02 20:50:41 2012 +0200
+++ b/src/Pure/Isar/named_target.ML	Mon Apr 02 21:49:27 2012 +0200
@@ -146,7 +146,7 @@
 (* declaration *)
 
 fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
-  if target = "" then Generic_Target.standard_declaration decl lthy
+  if target = "" then Generic_Target.theory_declaration decl lthy
   else
     lthy
     |> pervasive ? Generic_Target.background_declaration decl
diff -r daeaf4824e9a -r 4bab649dedf0 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Mon Apr 02 20:50:41 2012 +0200
+++ b/src/Pure/Isar/overloading.ML	Mon Apr 02 21:49:27 2012 +0200
@@ -207,7 +207,7 @@
         abbrev = Generic_Target.abbrev
           (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
             Generic_Target.theory_abbrev prmode ((b, mx), t)),
-        declaration = K Generic_Target.standard_declaration,
+        declaration = K Generic_Target.theory_declaration,
         pretty = pretty,
         exit = Local_Theory.target_of o conclude}
   end;