changeset 60948 | b710a5087116 |
parent 60819 | e1f1842bf344 |
child 61508 | 2c7e2ae6173d |
--- a/src/Pure/goal.ML Sun Aug 16 17:11:31 2015 +0200 +++ b/src/Pure/goal.ML Sun Aug 16 18:19:30 2015 +0200 @@ -209,7 +209,7 @@ | SOME st => let val _ = - Theory.subthy (Thm.theory_of_thm st, thy) orelse + Context.subthy_id (Thm.theory_id_of_thm st, Context.theory_id thy) orelse err "Bad background theory of goal state"; val res = (finish ctxt' st