# HG changeset patch
# User wenzelm
# Date 1449570537 -3600
# Node ID 71446a608dfdc991b7477acbba628afd9e1c1f92
# Parent  1530a0f195394f00edeaf8365770ff170b438006
tuned;

diff -r 1530a0f19539 -r 71446a608dfd src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Dec 08 10:49:08 2015 +0100
+++ b/src/Pure/Isar/method.ML	Tue Dec 08 11:28:57 2015 +0100
@@ -694,7 +694,7 @@
   setup @{binding "-"} (Scan.succeed (K insert_facts))
     "insert current facts, nothing else" #>
   setup @{binding goal_cases} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn ctxt =>
-    METHOD_CASES (fn facts => fn st =>
+    METHOD_CASES (fn _ => fn st =>
       let
         val _ =
           (case drop (Thm.nprems_of st) names of