# HG changeset patch
# User obua
# Date 1127598917 -7200
# Node ID bab7bf6554f4d1022943f20a7705fe0f6e1b3856
# Parent  f8ea8068c6d9f55c251aaddb4ac221e410288a6c
set show_types and show_sorts during import

diff -r f8ea8068c6d9 -r bab7bf6554f4 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Sat Sep 24 21:13:15 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Sat Sep 24 23:55:17 2005 +0200
@@ -1216,7 +1216,7 @@
 			 if_debug prin isaconc)
 		val cs = non_trivial_term_consts isaconc
 		val _ = (message "Looking for consts:";
-			 writeln (commas cs))
+			 message (commas cs))
 		val pot_thms = Shuffler.find_potential thy isaconc
 		val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems")
 	    in