src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 26343 0dd2eab7b296
parent 26336 a0e2b706ce73
child 26435 bdce320cd426
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Mar 19 22:50:42 2008 +0100
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Mar 20 00:20:44 2008 +0100
     1.3 @@ -712,7 +712,7 @@
     1.4                     What we want is mapping onto simple PGIP name/context model. *)
     1.5                  val ctx = Toplevel.context_of (Toplevel.get_state()) (* NB: raises UNDEF *)
     1.6                  val thy = Context.theory_of_proof ctx
     1.7 -                val ths = [PureThy.get_thm thy (Facts.Named (thmname, NONE))]
     1.8 +                val ths = [PureThy.get_thm thy thmname]
     1.9                  val deps = filter_out (equal "")
    1.10                                        (Symtab.keys (fold Proofterm.thms_of_proof
    1.11                                                           (map Thm.proof_of ths) Symtab.empty))
    1.12 @@ -764,7 +764,7 @@
    1.13                                          [] (* asms *)
    1.14                                          th))
    1.15  
    1.16 -        fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Facts.Named (name, NONE)))
    1.17 +        fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name)
    1.18  
    1.19          val string_of_thy = Output.output o
    1.20                                  Pretty.string_of o (ProofDisplay.pretty_full_theory false)