# HG changeset patch
# User wenzelm
# Date 1450776935 -3600
# Node ID 77fa1ae5fd31e6290396fc2130a896b3d94f3b0c
# Parent  6c7861f783fd08875d6cf2f20531f3b761c8972a
tuned signature;

diff -r 6c7861f783fd -r 77fa1ae5fd31 src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Tue Dec 22 10:32:59 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML	Tue Dec 22 10:35:35 2015 +0100
@@ -20,9 +20,9 @@
   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 ->
+  val method: binding -> (binding * typ option * mixfix) list ->
     binding list -> binding list -> binding list -> Token.src -> local_theory -> local_theory
-  val method_definition_cmd: binding -> (binding * string option * mixfix) list ->
+  val method_cmd: binding -> (binding * string option * mixfix) list ->
     binding list -> binding list -> binding list -> Token.src -> local_theory -> local_theory
 end;
 
@@ -256,8 +256,7 @@
 
 local
 
-fun gen_method_definition add_fixes
-    name vars uses declares methods source lthy =
+fun gen_method add_fixes name vars uses declares methods source lthy =
   let
     val (uses_internal, lthy1) = lthy
       |> Proof_Context.concealed
@@ -314,8 +313,8 @@
 
 in
 
-val method_definition = gen_method_definition Proof_Context.add_fixes;
-val method_definition_cmd = gen_method_definition Proof_Context.add_fixes_cmd;
+val method = gen_method Proof_Context.add_fixes;
+val method_cmd = gen_method Proof_Context.add_fixes_cmd;
 
 end;
 
@@ -327,6 +326,6 @@
       (Scan.optional (@{keyword "declares"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
       Parse.!!! (@{keyword "="} |-- Parse.args1 (K true)) >>
       (fn ((((name, vars), (methods, uses)), declares), src) =>
-        method_definition_cmd name vars uses declares methods src));
+        method_cmd name vars uses declares methods src));
 
 end;