src/Pure/ProofGeneral/proof_general_pgip.ML

             let
                 (* TODO: interim: this is probably not right.
                    What we want is mapping onto simple PGIP name/context model. *)
                 val ctx = Toplevel.context_of (Toplevel.get_state()) (* NB: raises UNDEF *)
                 val thy = Context.theory_of_proof ctx
-                val ths = [PureThy.get_thm thy (PureThy.Name thmname)]
+                val ths = [PureThy.get_thm thy (Facts.Named (thmname, NONE))]
                 val deps = filter_out (equal "")
                                       (Symtab.keys (fold Proofterm.thms_of_proof
                                                          (map Thm.proof_of ths) Symtab.empty))
             in
                 if null deps then ()

                                         false (* quote *)
                                         false (* show hyps *)
                                         [] (* asms *)
                                         th))
 
-        fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Name name))
+        fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Facts.Named (name, NONE)))
 
         val string_of_thy = Output.output o
                                 Pretty.string_of o (ProofDisplay.pretty_full_theory false)
     in
         case (thyname, objtype) of