--- a/src/HOL/Tools/res_reconstruct.ML Fri May 16 23:25:37 2008 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Sat May 17 13:54:30 2008 +0200
@@ -38,7 +38,7 @@
fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
else ();
-val string_of_thm = PrintMode.setmp [] string_of_thm;
+val string_of_thm = PrintMode.setmp [] Display.string_of_thm;
(*For generating structured proofs: keep every nth proof line*)
val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" 1;