diff -r 6527ba893bae -r 7725da65f8e0 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Fri Sep 23 18:47:47 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Fri Sep 23 20:13:54 2005 +0200
@@ -1177,7 +1177,7 @@
 
 fun get_isabelle_thm thyname thmname hol4conc thy =
     let
-	val _ = message "get_isabelle_thm called..."
+	val _ = writeln ("get_isabelle_thm called: "^thmname)
 	val sg = sign_of thy
 
 	val (info,hol4conc') = disamb_term hol4conc
@@ -1196,7 +1196,7 @@
 	case get_hol4_mapping thyname thmname thy of
 	    SOME (SOME thmname) =>
 	    let
-		val _ = message ("Looking for " ^ thmname)
+		val _ = writeln ("Looking for " ^ thmname)
 		val th1 = (SOME (transform_error (PureThy.get_thm thy) (Name thmname))
 			   handle ERROR_MESSAGE _ =>
 				  (case split_name thmname of
@@ -1213,14 +1213,14 @@
 	    end
 	  | SOME NONE => error ("Trying to access ignored theorem " ^ thmname)
 	  | NONE =>
-	    let
-		val _ = (message "Looking for conclusion:";
+	    let		
+		val _ = (writeln "Looking for conclusion:";
 			 if_debug prin isaconc)
 		val cs = non_trivial_term_consts isaconc
-		val _ = (message "Looking for consts:";
-			 message (commas cs))
+		val _ = (writeln "Looking for consts:";
+			 writeln (commas cs))
 		val pot_thms = Shuffler.find_potential thy isaconc
-		val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems")
+		val _ = writeln ((Int.toString (length pot_thms)) ^ " potential theorems")
 	    in
 		case Shuffler.set_prop thy isaconc pot_thms of
 		    SOME (isaname,th) =>