proper full name within the name space of the method definition;

--- a/src/HOL/Eisbach/method_closure.ML	Tue Dec 22 16:35:41 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML	Tue Dec 22 17:14:35 2015 +0100
@@ -254,7 +254,6 @@
       |> add_fixes vars |-> fold_map Proof_Context.inferred_param |>> map Free;
 
     val (named_thms, modifiers) = map (check_attrib lthy2) (declares @ uses) |> split_list;
-    val method_name = Local_Theory.full_name lthy2 name;
     val method_names = map (Local_Theory.full_name lthy2) methods;
 
     fun parser args eval =
@@ -294,7 +293,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
+    |> pair (Local_Theory.full_name lthy name)
   end;
 
 in