src/HOL/Tools/res_atp.ML
changeset 22724 3002683a6e0f
parent 22645 8a70bc644833
child 22731 abfdccaed085
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Apr 17 21:06:59 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Apr 18 11:14:09 2007 +0200
     1.3 @@ -718,7 +718,7 @@
     1.4  (*Called by the oracle-based methods declared in res_atp_methods.ML*)
     1.5  fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
     1.6      let val conj_cls = make_clauses conjectures
     1.7 -                         |> ResAxioms.assume_abstract_list |> Meson.finish_cnf
     1.8 +                         |> ResAxioms.assume_abstract_list true |> Meson.finish_cnf
     1.9          val hyp_cls = cnf_hyps_thms ctxt
    1.10          val goal_cls = conj_cls@hyp_cls
    1.11          val goal_tms = map prop_of goal_cls