src/HOL/Modelcheck/mucke_oracle.ML

 in elim_quant_in_list sign DefsOk
 end;
 
 fun string_of_terms sign terms =
 let fun make_string sign [] = "" |
- 	make_string sign (trm::list) = 
-           ((Sign.string_of_term sign trm) ^ "\n" ^(make_string sign list))
+ 	make_string sign (trm::list) =
+           ((Output.output (Sign.string_of_term sign trm)) ^ "\n" ^(make_string sign list))
 in
 (setmp print_mode ["Mucke"] (make_string sign) terms)
 end;
 
 fun callmc s =