--- 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)))
--- 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) =>