src/HOL/Tools/res_atp.ML
changeset 24300 e170cee91c66
parent 24287 c857dac06da6
child 24320 ea5be4be3bae
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Aug 16 21:52:08 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Aug 17 00:03:50 2007 +0200
     1.3 @@ -768,7 +768,7 @@
     1.4  
     1.5  (*Called by the oracle-based methods declared in res_atp_methods.ML*)
     1.6  fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
     1.7 -    let val conj_cls = make_clauses conjectures
     1.8 +    let val conj_cls = Meson.make_clauses conjectures
     1.9                           |> ResAxioms.assume_abstract_list "subgoal" |> Meson.finish_cnf
    1.10          val hyp_cls = cnf_hyps_thms ctxt
    1.11          val goal_cls = conj_cls@hyp_cls