# HG changeset patch
# User haftmann
# Date 1417708314 -3600
# Node ID 15f7ebb29d38b7c3f58d58906817e00dce4b8a81
# Parent  3100a7b1c092993c41ef89fd5422e525c471c08b
tuned variable names

diff -r 3100a7b1c092 -r 15f7ebb29d38 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Thu Dec 04 16:51:54 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Thu Dec 04 16:51:54 2014 +0100
@@ -170,7 +170,7 @@
     val concl = Logic.concl_of_goal goal 1;
   in
     (case is_matching_thm extract_intro ctxt true concl thm of
-      SOME ss => SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, ss)
+      SOME k => SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, k)
     | NONE => NONE)
   end;
 
@@ -244,7 +244,7 @@
   let
     fun msub bounds obj = Pattern.matches thy (pat, obj) orelse
       (case obj of
-        Abs (x, T, t) => msub (bounds + 1) (snd (Term.dest_abs (Name.bound bounds, T, t)))
+        Abs (_, T, t) => msub (bounds + 1) (snd (Term.dest_abs (Name.bound bounds, T, t)))
       | t $ u => msub bounds t orelse msub bounds u
       | _ => false)
   in msub 0 obj end;
@@ -572,3 +572,4 @@
     else error "Unknown context");
 
 end;
+