--- a/src/HOL/Import/import_package.ML Mon Sep 26 15:56:28 2005 +0200
+++ b/src/HOL/Import/import_package.ML Mon Sep 26 16:10:19 2005 +0200
@@ -53,8 +53,9 @@
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) =>