# HG changeset patch
# User obua
# Date 1127561200 -7200
# Node ID 1c1557f7ae5cbb4f0796b05d99cd146b75b338a3
# Parent  1539d18e3e9fe5ecadf4d3bd498b26e649b61a33
remove debug clutter

diff -r 1539d18e3e9f -r 1c1557f7ae5c src/HOL/Import/import_package.ML
--- a/src/HOL/Import/import_package.ML	Sat Sep 24 13:11:05 2005 +0200
+++ b/src/HOL/Import/import_package.ML	Sat Sep 24 13:26:40 2005 +0200
@@ -39,7 +39,6 @@
      fn thy =>
      fn th =>
 	let
-	    val message = writeln
             val sg = sign_of_thm th
 	    val prem = hd (prems_of th)
 	    val _ = message ("Import trying to prove " ^ (string_of_cterm (cterm_of sg prem)))
diff -r 1539d18e3e9f -r 1c1557f7ae5c src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Sat Sep 24 13:11:05 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Sat Sep 24 13:26:40 2005 +0200
@@ -1177,7 +1177,6 @@
 
 fun get_isabelle_thm thyname thmname hol4conc thy =
     let
-	val _ = writeln ("get_isabelle_thm called: "^thmname)
 	val sg = sign_of thy
 
 	val (info,hol4conc') = disamb_term hol4conc
@@ -1196,7 +1195,6 @@
 	case get_hol4_mapping thyname thmname thy of
 	    SOME (SOME thmname) =>
 	    let
-		val _ = writeln ("Looking for " ^ thmname)
 		val th1 = (SOME (transform_error (PureThy.get_thm thy) (Name thmname))
 			   handle ERROR_MESSAGE _ =>
 				  (case split_name thmname of
@@ -1214,13 +1212,13 @@
 	  | SOME NONE => error ("Trying to access ignored theorem " ^ thmname)
 	  | NONE =>
 	    let		
-		val _ = (writeln "Looking for conclusion:";
+		val _ = (message "Looking for conclusion:";
 			 if_debug prin isaconc)
 		val cs = non_trivial_term_consts isaconc
-		val _ = (writeln "Looking for consts:";
+		val _ = (message "Looking for consts:";
 			 writeln (commas cs))
 		val pot_thms = Shuffler.find_potential thy isaconc
-		val _ = writeln ((Int.toString (length pot_thms)) ^ " potential theorems")
+		val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems")
 	    in
 		case Shuffler.set_prop thy isaconc pot_thms of
 		    SOME (isaname,th) =>