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 65458 cf504b7a7aa7
parent 64567 7141a3a4dc83
child 67721 5348bea4accd 
--- a/src/Pure/goal.ML	Mon Apr 10 16:43:12 2017 +0200
+++ b/src/Pure/goal.ML	Mon Apr 10 21:05:31 2017 +0200
@@ -210,7 +210,7 @@
       | SOME st =>
           let
             val _ =
-              Context.subthy_id (Thm.theory_id_of_thm st, Context.theory_id thy) orelse
+              Context.subthy_id (Thm.theory_id st, Context.theory_id thy) orelse
                 err "Bad background theory of goal state";
             val res =
               (finish ctxt' st
isabelle