src/Pure/Tools/find_theorems.ML
 changeset 30318 3d03190d2864 parent 30234 7dd251bce291 child 30364 577edc39b501
```     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Mar 06 21:49:58 2009 +0100
1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Mar 06 22:32:27 2009 +0100
1.3 @@ -168,8 +168,7 @@
1.4      fun etacn thm i = Seq.take (! tac_limit) o etac thm i;
1.5      fun try_thm thm =
1.6        if Thm.no_prems thm then rtac thm 1 goal
1.7 -      else (etacn thm THEN_ALL_NEW
1.8 -             (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
1.9 +      else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
1.10    in
1.11      fn (_, thm) =>
1.12        if (is_some o Seq.pull o try_thm) thm
1.13 @@ -181,11 +180,10 @@
1.14
1.15  fun filter_simp ctxt t (_, thm) =
1.16    let
1.17 -    val (_, {mk_rews = {mk, ...}, ...}) =
1.18 -      Simplifier.rep_ss (Simplifier.local_simpset_of ctxt);
1.19 +    val mksimps = Simplifier.mksimps (Simplifier.local_simpset_of ctxt);
1.20      val extract_simp =
1.21 -      (map Thm.full_prop_of o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl);
1.22 -    val ss = is_matching_thm extract_simp ctxt false t thm
1.23 +      (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
1.24 +    val ss = is_matching_thm extract_simp ctxt false t thm;
1.25    in
1.26      if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
1.27    end;
```