tuned variable names
authorhaftmann
Thu Dec 04 16:51:54 2014 +0100 (2014-12-04)
changeset 5909615f7ebb29d38
parent 59095 3100a7b1c092
child 59097 4b05ce4c84b0
tuned variable names
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Dec 04 16:51:54 2014 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Dec 04 16:51:54 2014 +0100
     1.3 @@ -170,7 +170,7 @@
     1.4      val concl = Logic.concl_of_goal goal 1;
     1.5    in
     1.6      (case is_matching_thm extract_intro ctxt true concl thm of
     1.7 -      SOME ss => SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, ss)
     1.8 +      SOME k => SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, k)
     1.9      | NONE => NONE)
    1.10    end;
    1.11  
    1.12 @@ -244,7 +244,7 @@
    1.13    let
    1.14      fun msub bounds obj = Pattern.matches thy (pat, obj) orelse
    1.15        (case obj of
    1.16 -        Abs (x, T, t) => msub (bounds + 1) (snd (Term.dest_abs (Name.bound bounds, T, t)))
    1.17 +        Abs (_, T, t) => msub (bounds + 1) (snd (Term.dest_abs (Name.bound bounds, T, t)))
    1.18        | t $ u => msub bounds t orelse msub bounds u
    1.19        | _ => false)
    1.20    in msub 0 obj end;
    1.21 @@ -572,3 +572,4 @@
    1.22      else error "Unknown context");
    1.23  
    1.24  end;
    1.25 +