src/HOL/Import/hol4rews.ML

--- a/src/HOL/Import/hol4rews.ML	Wed Jan 21 16:51:45 2009 +0100
+++ b/src/HOL/Import/hol4rews.ML	Wed Jan 21 18:27:43 2009 +0100
@@ -390,7 +390,7 @@
         val thm2 = standard thm1;
       in
         thy
-        |> PureThy.store_thm (bthm, thm2)
+        |> PureThy.store_thm (Binding.name bthm, thm2)
         |> snd
         |> add_hol4_theorem bthy bthm hth
       end;