src/HOL/Import/hol4rews.ML

     val rews = HOL4Rewrites.get thy;
     val pending = HOL4Pending.get thy;
     fun process ((bthy,bthm), hth as (_,thm)) thy =
       let
         val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm);
-        val thm2 = standard thm1;
+        val thm2 = Drule.standard thm1;
       in
         thy
         |> PureThy.store_thm (Binding.name bthm, thm2)
         |> snd
         |> add_hol4_theorem bthy bthm hth