changeset 65458 | cf504b7a7aa7 |
parent 64567 | 7141a3a4dc83 |
child 67119 | acb0807ddb56 |
--- a/src/Pure/Isar/proof.ML Mon Apr 10 16:43:12 2017 +0200 +++ b/src/Pure/Isar/proof.ML Mon Apr 10 21:05:31 2017 +0200 @@ -515,7 +515,7 @@ val thy = Proof_Context.theory_of ctxt; val _ = - Context.subthy_id (Thm.theory_id_of_thm goal, Context.theory_id thy) orelse + Context.subthy_id (Thm.theory_id goal, Context.theory_id thy) orelse error "Bad background theory of goal state"; val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);