1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Oct 20 20:54:31 2009 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Oct 20 21:22:37 2009 +0200
     1.3 @@ -613,7 +613,7 @@
     1.4                  (* TODO: interim: this is probably not right.
     1.5                     What we want is mapping onto simple PGIP name/context model. *)
     1.6                  val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
     1.7 -                val thy = Context.theory_of_proof ctx
     1.8 +                val thy = ProofContext.theory_of ctx
     1.9                  val ths = [PureThy.get_thm thy thmname]
    1.10                  val deps = #2 (thms_deps ths);
    1.11              in