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
```