src/Pure/goal.ML

       (case SINGLE (tac' {prems = prems, context = ctxt'}) (init stmt) of
         NONE => err "Tactic failed"
       | 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
                 |> Drule.flexflex_unique (SOME ctxt')
                 |> Thm.check_shyps ctxt'