diff -r 2405ab06d5b1 -r fcf3bb1b54e1 src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Tue Jan 12 11:00:55 2016 +1100
+++ b/src/HOL/Eisbach/match_method.ML	Tue Jan 12 11:03:40 2016 +1100
@@ -434,8 +434,6 @@
       |> add_focus_schematics (snd schematics)
       |> fold_map add_focus_prem (rev prems)
 
-    val local_prems = map2 pair prem_ids (rev prems);
-
   in
     (prem_ids,
       {context = ctxt',