diff -r 245955f0c579 -r 267cc670317a src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Sun Jun 20 09:28:35 2004 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Sun Jun 20 09:30:12 2004 +0200
@@ -487,7 +487,7 @@
 fun string_of_terms sign terms =
 let fun make_string sign [] = "" |
  	make_string sign (trm::list) =
-           ((Output.output (Sign.string_of_term sign trm)) ^ "\n" ^(make_string sign list))
+           Sign.string_of_term sign trm ^ "\n" ^ make_string sign list
 in
 (setmp print_mode ["Mucke"] (make_string sign) terms)
 end;