# HG changeset patch
# User wenzelm
# Date 1427967674 -7200
# Node ID 6c0f6249069950d8fb7f952de851cc830cfeb59c
# Parent  158c4123f5cc37c3ae09a99d93d65032d687654d
tuned signature;

diff -r 158c4123f5cc -r 6c0f62490699 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Apr 02 11:28:59 2015 +0200
+++ b/src/Pure/Isar/method.ML	Thu Apr 02 11:41:14 2015 +0200
@@ -56,6 +56,7 @@
   val finish_text: text option * bool -> text
   val print_methods: Proof.context -> unit
   val check_name: Proof.context -> xstring * Position.T -> string
+  val check_src: Proof.context -> Token.src -> Token.src
   val method_syntax: (Proof.context -> method) context_parser ->
     Token.src -> Proof.context -> method
   val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
@@ -367,8 +368,8 @@
   let val context = Context.Proof ctxt
   in #1 o Name_Space.check context (get_methods context) end;
 
-fun check_src ctxt src =
-  Token.check_src ctxt (get_methods (Context.Proof ctxt)) src;
+fun check_src ctxt =
+  #1 o Token.check_src ctxt (get_methods (Context.Proof ctxt));
 
 
 (* method setup *)
@@ -396,7 +397,7 @@
 
 fun method_closure ctxt0 src0 =
   let
-    val (src1, _) = check_src ctxt0 src0;
+    val src1 = check_src ctxt0 src0;
     val src2 = Token.init_assignable_src src1;
     val ctxt = Context_Position.not_really ctxt0;
     val _ = Seq.pull (method ctxt src2 ctxt [] (Goal.protect 0 Drule.dummy_thm));
@@ -568,7 +569,7 @@
         NONE => (Parse.xname, Token.src)
       | SOME ctxt =>
          (Args.checked_name (fn (xname, _) => check_name ctxt (xname, Position.none)),
-          fn name => fn args => #1 (check_src ctxt (Token.src name args))));
+          fn name => fn args => check_src ctxt (Token.src name args)));
 
     fun meth5 x =
      (Parse.position meth_name >> (fn name => Source (mk_src name [])) ||