src/Pure/goal.ML
changeset 65458 cf504b7a7aa7
parent 64567 7141a3a4dc83
child 67721 5348bea4accd
     1.1 --- a/src/Pure/goal.ML	Mon Apr 10 16:43:12 2017 +0200
     1.2 +++ b/src/Pure/goal.ML	Mon Apr 10 21:05:31 2017 +0200
     1.3 @@ -210,7 +210,7 @@
     1.4        | SOME st =>
     1.5            let
     1.6              val _ =
     1.7 -              Context.subthy_id (Thm.theory_id_of_thm st, Context.theory_id thy) orelse
     1.8 +              Context.subthy_id (Thm.theory_id st, Context.theory_id thy) orelse
     1.9                  err "Bad background theory of goal state";
    1.10              val res =
    1.11                (finish ctxt' st