src/HOL/Tools/res_atp.ML
changeset 24634 38db11874724
parent 24612 d1b315bdb8d7
child 24827 646bdc51eb7d
--- a/src/HOL/Tools/res_atp.ML	Tue Sep 18 18:05:34 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML	Tue Sep 18 18:05:37 2007 +0200
@@ -946,7 +946,7 @@
       val ctxt = ProofContext.init (theory_of_thm th)
   in  isar_atp (ctxt, [], th)  end;
 
-val isar_atp_writeonly = PrintMode.with_default
+val isar_atp_writeonly = PrintMode.setmp []
       (fn (ctxt, chain_ths, th) =>
        if Thm.no_prems th then ()
        else