src/HOL/Tools/res_reconstruct.ML

   | have_or_show have lname = have ^ lname ^ ": \""
 
 (*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
   ATP may have their literals reordered.*)
 fun isar_lines ctxt ctms =
-  let val string_of = Syntax.string_of_term ctxt
+  let val string_of = PrintMode.setmp [] (fn term => Syntax.string_of_term ctxt term)
       val _ = trace ("\n\nisar_lines: start\n")
       fun doline have (lname, t, []) =  (*No deps: it's a conjecture clause, with no proof.*)
            (case permuted_clause t ctms of
                 SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
               | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n")  (*no match!!*)