# HG changeset patch
# User wenzelm
# Date 1408620691 -7200
# Node ID 83599179e6eb3879a7b4bc8de67a8724b1486328
# Parent  d41e3d0ac50c7c1d9c86efbbb21c212a84fe065b
tuned;

diff -r d41e3d0ac50c -r 83599179e6eb src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Aug 21 10:07:06 2014 +0200
+++ b/src/Pure/Isar/method.ML	Thu Aug 21 13:31:31 2014 +0200
@@ -392,7 +392,7 @@
 
 fun method_closure ctxt0 src0 =
   let
-    val (src1, meth) = 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));