changeset 21646 | c07b5b0e8492 |
parent 21603 | 0fa36ea9aaf5 |
child 22109 | 9188aed2c3ca |
--- a/src/Pure/drule.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/drule.ML Tue Dec 05 00:30:38 2006 +0100 @@ -427,7 +427,7 @@ | _ => raise THM("flexflex_unique: multiple unifiers", 0, [th]); fun close_derivation thm = - if Thm.get_name_tags thm = ("", []) then Thm.name_thm ("", thm) + if Thm.get_name thm = "" then Thm.put_name "" thm else thm;