src/HOL/Import/import_package.ML

 	    val thm = snd (ProofKernel.to_isa_thm hol4thm)
 	    val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy
 	    val thm = equal_elim rew thm
 	    val prew = ProofKernel.rewrite_hol4_term prem thy
 	    val prem' = #2 (Logic.dest_equals (prop_of prew))
+            val _ = message ("Import proved " ^ (string_of_thm thm))    
             val thm = Drule.disambiguate_frees thm
-	    val _ = message ("Import proved " ^ (string_of_thm thm))  
+	    val _ = message ("Disambiguate: " ^ (string_of_thm thm))  
 	in
 	    case Shuffler.set_prop thy prem' [("",thm)] of
 		SOME (_,thm) =>
 		let
 		    val _ = if prem' aconv (prop_of thm)