| changeset 64568 | a504a3dec35a |
| parent 64556 | 851ae0e7b09c |
| child 64574 | 1134e4d5e5b7 |
--- a/src/Pure/more_thm.ML Wed Dec 14 16:59:41 2016 +0100 +++ b/src/Pure/more_thm.ML Wed Dec 14 18:22:18 2016 +0100 @@ -452,8 +452,7 @@ (* close_derivation *) fun close_derivation thm = - if Thm.derivation_name thm = "" then Thm.name_derivation "" thm - else thm; + if Thm.derivation_closed thm then thm else Thm.name_derivation "" thm; (* user renaming of parameters in a subgoal *)