src/HOL/Import/hol4rews.ML

       let
         val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm);
         val thm2 = standard thm1;
       in
         thy
-        |> PureThy.store_thm ((bthm, thm2), [])
+        |> PureThy.store_thm (bthm, thm2)
         |> snd
         |> add_hol4_theorem bthy bthm hth
       end;
   in
     thy