--- a/src/Pure/pure_thy.ML Sat May 08 17:10:27 2010 +0200
+++ b/src/Pure/pure_thy.ML Sat May 08 16:53:53 2010 +0200
@@ -121,7 +121,7 @@
| name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
fun name_thm pre official name thm = thm
- |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name)
+ |> not (Thm.derivation_name thm <> "" andalso pre orelse not official) ? Thm.name_derivation name
|> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name);
fun name_thms pre official name xs =