src/Pure/pure_thy.ML
changeset 26050 88bb26089ef5
parent 25981 870ae1d0452e
child 26282 305d5ca4fa9d
--- a/src/Pure/pure_thy.ML	Sat Feb 09 12:56:12 2008 +0100
+++ b/src/Pure/pure_thy.ML	Sun Feb 10 20:49:42 2008 +0100
@@ -345,7 +345,8 @@
 
 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)
-  |> (if has_name_hint thm andalso pre orelse name = "" then I else put_name_hint name);
+  |> (if has_name_hint thm andalso pre orelse name = "" then I else put_name_hint name)
+  |> Thm.map_tags (Position.default_properties (Position.thread_data ()));
 
 fun name_thms pre official name xs =
   map (uncurry (name_thm pre official)) (name_multi name xs);