src/Pure/Tools/find_theorems.ML
changeset 33029 2fefe039edf1
parent 32859 204f749f35a9
child 33036 c61fe520602b
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Oct 20 20:03:23 2009 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Oct 20 20:54:31 2009 +0200
     1.3 @@ -109,7 +109,7 @@
     1.4        in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
     1.5  
     1.6      fun bestmatch [] = NONE
     1.7 -      | bestmatch xs = SOME (foldr1 Int.min xs);
     1.8 +      | bestmatch xs = SOME (foldl1 Int.min xs);
     1.9  
    1.10      val match_thm = matches o refine_term;
    1.11    in
    1.12 @@ -142,7 +142,7 @@
    1.13      (*dest rules always have assumptions, so a dest with one
    1.14        assumption is as good as an intro rule with none*)
    1.15      if not (null successful)
    1.16 -    then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE
    1.17 +    then SOME (Thm.nprems_of thm - 1, foldl1 Int.min successful) else NONE
    1.18    end;
    1.19  
    1.20  fun filter_intro doiff ctxt goal (_, thm) =
    1.21 @@ -173,7 +173,7 @@
    1.22          assumption is as good as an intro rule with none*)
    1.23        if is_nontrivial (ProofContext.theory_of ctxt) (Thm.major_prem_of thm)
    1.24          andalso not (null successful)
    1.25 -      then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE
    1.26 +      then SOME (Thm.nprems_of thm - 1, foldl1 Int.min successful) else NONE
    1.27      end
    1.28    else NONE
    1.29