changeset 28814 | 463c9e9111ae |
parent 28809 | 7c2e1bbf3c36 |
child 28817 | c8cc94a470d4 |
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Nov 16 18:19:27 2008 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Nov 16 20:03:42 2008 +0100 @@ -254,7 +254,7 @@ thms |> fold (fn (_, ((name, _, _), _)) => name <> "" ? Symtab.update (name, ())); fun add_thm th = - (case Thm.proof_of th of + (case Thm.proof_body_of th of PBody {proof = PThm (_, ((name, _, _), body)), ...} => if Thm.has_name_hint th andalso Thm.get_name_hint th = name then add_proof_body (Lazy.force body)