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/goal.ML
changeset 54984 da70ab8531f4
parent 54981 a128df2f670e
child 54985 9a1710a64412 
--- a/src/Pure/goal.ML	Fri Jan 10 17:44:41 2014 +0100
+++ b/src/Pure/goal.ML	Fri Jan 10 21:37:28 2014 +0100
@@ -221,7 +221,7 @@
               (finish ctxt' st
                 |> Drule.flexflex_unique
                 |> Thm.check_shyps sorts
-                (* |> Assumption.check_hyps ctxt' FIXME *))
+                |> Thm.check_hyps ctxt')
               handle THM (msg, _, _) => err msg | ERROR msg => err msg;
           in
             if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res] then res
isabelle