--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Mar 19 22:27:57 2008 +0100
@@ -712,7 +712,7 @@
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))
@@ -764,7 +764,7 @@
[] (* 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)