Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Tools/find_theorems.ML
changeset 30234 7dd251bce291
parent 30216 0300b7420b07
child 30318 3d03190d2864 
--- a/src/Pure/Tools/find_theorems.ML	Tue Mar 03 21:53:52 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Wed Mar 04 00:05:20 2009 +0100
@@ -169,8 +169,7 @@
     fun try_thm thm =
       if Thm.no_prems thm then rtac thm 1 goal
       else (etacn thm THEN_ALL_NEW
-             (Goal.norm_hhf_tac THEN'
-               Method.assumption_tac ctxt)) 1 goal;
+             (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
   in
     fn (_, thm) =>
       if (is_some o Seq.pull o try_thm) thm
isabelle