localized command 'method_setup' and 'attribute_setup';
clarified (non)application of morphism: argument src is already transformed, semantic body remains untransformed;

--- a/NEWS	Thu Aug 14 12:49:49 2014 +0200
+++ b/NEWS	Thu Aug 14 14:28:11 2014 +0200
@@ -4,6 +4,12 @@
 New in this Isabelle version
 ----------------------------
 
+*** General ***
+
+* Commands 'method_setup' and 'attribute_setup' now work within a
+local theory context.
+
+
 *** HOL ***
 
 * Sledgehammer:

--- a/src/Doc/Isar_Ref/Proof.thy	Thu Aug 14 12:49:49 2014 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Thu Aug 14 14:28:11 2014 +0200
@@ -915,7 +915,7 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def "method_setup"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def "method_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   \end{matharray}
 
   @{rail \<open>
@@ -925,7 +925,7 @@
   \begin{description}
 
   \item @{command "method_setup"}~@{text "name = text description"}
-  defines a proof method in the current theory.  The given @{text
+  defines a proof method in the current context.  The given @{text
   "text"} has to be an ML expression of type
   @{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\
   basic parsers defined in structure @{ML_structure Args} and @{ML_structure

--- a/src/Doc/Isar_Ref/Spec.thy	Thu Aug 14 12:49:49 2014 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Thu Aug 14 14:28:11 2014 +0200
@@ -1031,7 +1031,7 @@
     @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
     @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
-    @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def "attribute_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   \end{matharray}
   \begin{tabular}{rcll}
     @{attribute_def ML_print_depth} & : & @{text attribute} & default 10 \\
@@ -1093,7 +1093,7 @@
   concrete outer syntax, for example.
 
   \item @{command "attribute_setup"}~@{text "name = text description"}
-  defines an attribute in the current theory.  The given @{text
+  defines an attribute in the current context.  The given @{text
   "text"} has to be an ML expression of type
   @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
   structure @{ML_structure Args} and @{ML_structure Attrib}.

--- a/src/Pure/Isar/attrib.ML	Thu Aug 14 12:49:49 2014 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Aug 14 14:28:11 2014 +0200
@@ -42,7 +42,8 @@
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
   val local_setup: Binding.binding -> attribute context_parser -> string ->
     local_theory -> local_theory
-  val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
+  val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
+    local_theory -> local_theory
   val internal: (morphism -> attribute) -> src
   val add_del: attribute -> attribute -> attribute context_parser
   val thm_sel: Facts.interval list parser
@@ -132,15 +133,12 @@
       Name_Space.define context true (binding, (att, comment)) (Attributes.get context);
   in (name, Context.the_theory (Attributes.put attribs' context)) end;
 
-fun define binding att comment lthy =
-  let val att0 = att o Args.transform_values (Local_Theory.background_morphism lthy) in
-    lthy
-    |> Local_Theory.background_theory_result (define_global binding att0 comment)
-    |-> (fn name =>
-      Local_Theory.map_contexts (K transfer_attributes)
-      #> Local_Theory.generic_alias Attributes.map binding name
-      #> pair name)
-  end;
+fun define binding att comment =
+  Local_Theory.background_theory_result (define_global binding att comment)
+  #-> (fn name =>
+    Local_Theory.map_contexts (K transfer_attributes)
+    #> Local_Theory.generic_alias Attributes.map binding name
+    #> pair name);
 
 
 (* check *)
@@ -207,12 +205,13 @@
 fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
 
 fun attribute_setup name source cmt =
-  Context.theory_map (ML_Context.expression (#pos source)
+  (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
+    ML_Lex.read_source false source @
+    ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
+  |> ML_Context.expression (#pos source)
     "val (name, scan, comment): binding * attribute context_parser * string"
-    "Context.map_theory (Attrib.setup name scan comment)"
-    (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
-      ML_Lex.read_source false source @
-      ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
+    "Context.map_proof (Attrib.local_setup name scan comment)"
+  |> Context.proof_map;
 
 
 (* internal attribute *)

--- a/src/Pure/Isar/isar_syn.ML	Thu Aug 14 12:49:49 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Aug 14 14:28:11 2014 +0200
@@ -329,16 +329,16 @@
     (Parse.ML_source >> Isar_Cmd.local_setup);
 
 val _ =
-  Outer_Syntax.command @{command_spec "attribute_setup"} "define attribute in ML"
+  Outer_Syntax.local_theory @{command_spec "attribute_setup"} "define attribute in ML"
     (Parse.position Parse.name --
         Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
-      >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
+      >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt));
 
 val _ =
-  Outer_Syntax.command @{command_spec "method_setup"} "define proof method in ML"
+  Outer_Syntax.local_theory @{command_spec "method_setup"} "define proof method in ML"
     (Parse.position Parse.name --
         Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
-      >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
+      >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt));
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "declaration"} "generic ML declaration"

--- a/src/Pure/Isar/local_theory.ML	Thu Aug 14 12:49:49 2014 +0200
+++ b/src/Pure/Isar/local_theory.ML	Thu Aug 14 14:28:11 2014 +0200
@@ -39,7 +39,6 @@
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
   val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val background_theory: (theory -> theory) -> local_theory -> local_theory
-  val background_morphism: local_theory -> morphism
   val target_of: local_theory -> Proof.context
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val target_morphism: local_theory -> morphism
@@ -106,7 +105,8 @@
   target: Proof.context};
 
 fun make_lthy (naming, operations, after_close, brittle, target) : lthy =
-  {naming = naming, operations = operations, after_close = after_close, brittle = brittle, target = target};
+  {naming = naming, operations = operations, after_close = after_close,
+    brittle = brittle, target = target};
 
 
 (* context data *)
@@ -226,9 +226,6 @@
 
 fun background_theory f = #2 o background_theory_result (f #> pair ());
 
-fun background_morphism lthy =
-  standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
-
 
 (* target contexts *)
 

--- a/src/Pure/Isar/method.ML	Thu Aug 14 12:49:49 2014 +0200
+++ b/src/Pure/Isar/method.ML	Thu Aug 14 14:28:11 2014 +0200
@@ -70,7 +70,8 @@
   val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
   val local_setup: binding -> (Proof.context -> method) context_parser -> string ->
     local_theory -> local_theory
-  val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
+  val method_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
+    local_theory -> local_theory
   type modifier = (Proof.context -> Proof.context) * attribute
   val section: modifier parser list -> thm list context_parser
   val sections: modifier parser list -> thm list list context_parser
@@ -350,15 +351,12 @@
       Name_Space.define context true (binding, (meth, comment)) (Methods.get context);
   in (name, Context.the_theory (Methods.put meths' context)) end;
 
-fun define binding meth comment lthy =
-  let val meth0 = meth o Args.transform_values (Local_Theory.background_morphism lthy) in
-    lthy
-    |> Local_Theory.background_theory_result (define_global binding meth0 comment)
-    |-> (fn name =>
-      Local_Theory.map_contexts (K transfer_methods)
-      #> Local_Theory.generic_alias Methods.map binding name
-      #> pair name)
-  end;
+fun define binding meth comment =
+  Local_Theory.background_theory_result (define_global binding meth comment)
+  #-> (fn name =>
+    Local_Theory.map_contexts (K transfer_methods)
+    #> Local_Theory.generic_alias Methods.map binding name
+    #> pair name);
 
 
 (* check *)
@@ -393,12 +391,13 @@
 fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
 
 fun method_setup name source cmt =
-  Context.theory_map (ML_Context.expression (#pos source)
+  (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
+    ML_Lex.read_source false source @
+    ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
+  |> ML_Context.expression (#pos source)
     "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
-    "Context.map_theory (Method.setup name scan comment)"
-    (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
-      ML_Lex.read_source false source @
-      ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
+    "Context.map_proof (Method.local_setup name scan comment)"
+  |> Context.proof_map;