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