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 60819 e1f1842bf344
parent 60723 757cad5a3fe9
child 60948 b710a5087116 
--- a/src/Pure/goal.ML	Tue Jul 28 19:49:54 2015 +0200
+++ b/src/Pure/goal.ML	Tue Jul 28 20:05:53 2015 +0200
@@ -214,7 +214,7 @@
             val res =
               (finish ctxt' st
                 |> Drule.flexflex_unique (SOME ctxt')
-                |> Thm.check_shyps sorts
+                |> Thm.check_shyps ctxt' sorts
                 |> Thm.check_hyps (Context.Proof ctxt'))
               handle THM (msg, _, _) => err msg | ERROR msg => err msg;
           in
isabelle