# HG changeset patch
# User wenzelm
# Date 1450800875 -3600
# Node ID fe2b7f4276be88297ee099be9ca013401022d35a
# Parent  ae36547d3a30b94ed266a1e19bbac819be4b0021
proper full name within the name space of the method definition;

diff -r ae36547d3a30 -r fe2b7f4276be src/HOL/Eisbach/method_closure.ML
--- 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