diff -r f21494dc0bf6 -r 9696218b02fe src/HOL/Import/import.ML
--- a/src/HOL/Import/import.ML	Sat Mar 03 23:54:44 2012 +0100
+++ b/src/HOL/Import/import.ML	Sun Mar 04 00:03:04 2012 +0100
@@ -37,11 +37,11 @@
                                NONE => fst (Replay.setup_int_thms thyname thy)
                              | SOME a => a
             val proof = snd (ProofKernel.import_proof thyname thmname thy) thy
-            val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
-            val thm = snd (ProofKernel.to_isa_thm hol4thm)
-            val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy
+            val importerthm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
+            val thm = snd (ProofKernel.to_isa_thm importerthm)
+            val rew = ProofKernel.rewrite_importer_term (concl_of thm) thy
             val thm = Thm.equal_elim rew thm
-            val prew = ProofKernel.rewrite_hol4_term prem thy
+            val prew = ProofKernel.rewrite_importer_term prem thy
             val prem' = #2 (Logic.dest_equals (prop_of prew))
             val _ = message ("Import proved " ^ Display.string_of_thm ctxt thm)
             val thm = ProofKernel.disambiguate_frees thm