# HG changeset patch
# User wenzelm
# Date 1449692128 -3600
# Node ID b8a3deee50dbf7fd975f36632de266f651683161
# Parent  e65344e3eeb5685ae79640f223338afc7e398b04
tuned signature;

diff -r e65344e3eeb5 -r b8a3deee50db src/HOL/Eisbach/eisbach_antiquotations.ML
--- a/src/HOL/Eisbach/eisbach_antiquotations.ML	Wed Dec 09 21:10:45 2015 +0100
+++ b/src/HOL/Eisbach/eisbach_antiquotations.ML	Wed Dec 09 21:15:28 2015 +0100
@@ -15,7 +15,7 @@
       (Args.context -- Scan.lift (Args.mode "drop_cases") -- Scan.lift (Parse.position Parse.name)
         >> (fn ((ctxt, drop_cases), nameref) =>
           let
-            val ((targs, (factargs, margs)), _) = Method_Closure.get_inner_method ctxt nameref;
+            val ((targs, (factargs, margs)), _) = Method_Closure.get_method ctxt nameref;
 
             val has_factargs = not (null factargs);
 
@@ -34,9 +34,9 @@
             val ML_context = ML_Context.struct_name ctxt ^ ".ML_context";
             val ml_inner =
               ML_Syntax.atomic
-                ("Method_Closure.get_inner_method " ^  ML_context ^
+                ("Method_Closure.get_method " ^  ML_context ^
                   ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position nameref ^
-                  "|> (fn ((targs, (_, margs)), text) => Method_Closure.eval_inner_method " ^
+                  "|> (fn ((targs, (_, margs)), text) => Method_Closure.eval_method " ^
                   ML_context ^ " ((targs, margs), text))");
 
             val drop_cases_suffix =
diff -r e65344e3eeb5 -r b8a3deee50db src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Wed Dec 09 21:10:45 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML	Wed Dec 09 21:15:28 2015 +0100
@@ -21,9 +21,9 @@
   val read_closure_input: Proof.context -> Input.source -> Method.text * Token.src
   val method_text: Method.text context_parser
   val method_evaluate: Method.text -> Proof.context -> Method.method
-  val get_inner_method: Proof.context -> string * Position.T ->
+  val get_method: Proof.context -> string * Position.T ->
     (term list * (string list * string list)) * Method.text
-  val eval_inner_method: Proof.context -> (term list * string list) * Method.text ->
+  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_definition: binding -> (binding * typ option * mixfix) list ->
@@ -276,7 +276,7 @@
           (map (Morphism_name phi) declares, map (Morphism_name phi) methods)),
           (Method.map_source o map) (Token.transform phi) text))));
 
-fun get_inner_method ctxt (xname, pos) =
+fun get_method ctxt (xname, pos) =
   let
     val name = Method.check_name ctxt (xname, pos);
   in
@@ -285,7 +285,7 @@
     | NONE => error ("Unknown Eisbach method: " ^ quote name ^ Position.here pos))
   end;
 
-fun eval_inner_method ctxt0 header fixes attribs methods =
+fun eval_method ctxt0 header fixes attribs methods =
   let
     val ((term_args, hmethods), text) = header;