src/Pure/Tools/find_theorems.ML
changeset 30234 7dd251bce291
parent 30216 0300b7420b07
child 30318 3d03190d2864
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Mar 03 21:53:52 2009 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Mar 04 00:05:20 2009 +0100
     1.3 @@ -169,8 +169,7 @@
     1.4      fun try_thm thm =
     1.5        if Thm.no_prems thm then rtac thm 1 goal
     1.6        else (etacn thm THEN_ALL_NEW
     1.7 -             (Goal.norm_hhf_tac THEN'
     1.8 -               Method.assumption_tac ctxt)) 1 goal;
     1.9 +             (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