# HG changeset patch
# User wenzelm
# Date 1450798541 -3600
# Node ID ae36547d3a30b94ed266a1e19bbac819be4b0021
# Parent  d5ead6bfa1ff34f58213b34fb9e537cc7e59dbaf
tuned signature;
tuned;

diff -r d5ead6bfa1ff -r ae36547d3a30 src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Tue Dec 22 16:34:57 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML	Tue Dec 22 16:35:41 2015 +0100
@@ -20,10 +20,10 @@
   val eval_method: Proof.context -> (term list * string list) * Method.text ->
     term list -> (string * thm list) list -> (Proof.context -> Method.method) list ->
     Proof.context -> Method.method
-  val method: binding -> (binding * typ option * mixfix) list ->
-    binding list -> binding list -> binding list -> Token.src -> local_theory -> local_theory
-  val method_cmd: binding -> (binding * string option * mixfix) list ->
-    binding list -> binding list -> binding list -> Token.src -> local_theory -> local_theory
+  val method: binding -> (binding * typ option * mixfix) list -> binding list ->
+    binding list -> binding list -> Token.src -> local_theory -> string * local_theory
+  val method_cmd: binding -> (binding * string option * mixfix) list -> binding list ->
+    binding list -> binding list -> Token.src -> local_theory -> string * local_theory
 end;
 
 structure Method_Closure: METHOD_CLOSURE =
@@ -161,7 +161,7 @@
 
 fun method_instantiate env text =
   let
-    val morphism = Morphism.term_morphism "instantiate_text" (Envir.norm_term env);
+    val morphism = Morphism.term_morphism "method_instantiate" (Envir.norm_term env);
     val text' = (Method.map_source o map) (Token.transform morphism) text;
   in method_evaluate text' end;
 
@@ -254,7 +254,8 @@
       |> add_fixes vars |-> fold_map Proof_Context.inferred_param |>> map Free;
 
     val (named_thms, modifiers) = map (check_attrib lthy2) (declares @ uses) |> split_list;
-    val self_name :: method_names = map (Local_Theory.full_name lthy2) (name :: methods);
+    val method_name = Local_Theory.full_name lthy2 name;
+    val method_names = map (Local_Theory.full_name lthy2) methods;
 
     fun parser args eval =
       apfst (Config.put_generic Method.old_section_parser true) #>
@@ -293,6 +294,7 @@
     |> Proof_Context.restore_naming lthy
     |> Method.local_setup name real_parser "(defined in Eisbach)"
     |> add_method name ((term_args', named_thms, method_names), text')
+    |> pair method_name
   end;
 
 in
@@ -310,6 +312,6 @@
       (Scan.optional (@{keyword "declares"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
       Parse.!!! (@{keyword "="} |-- Parse.args1 (K true)) >>
       (fn ((((name, vars), (methods, uses)), declares), src) =>
-        method_cmd name vars uses declares methods src));
+        #2 o method_cmd name vars uses declares methods src));
 
 end;