src/Pure/Tools/find_theorems.ML
changeset 54742 7a86358a3c0b
parent 53633 69f1221fc892
child 55669 4612c450b59c
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -237,7 +237,9 @@
     1.4        Seq.take (Options.default_int @{option find_theorems_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 (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt')) 1 goal';
     1.8 +      else
     1.9 +        (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac ctxt' THEN' Method.assm_tac ctxt'))
    1.10 +          1 goal';
    1.11    in
    1.12      fn Internal (_, thm) =>
    1.13          if is_some (Seq.pull (try_thm thm))