--- a/src/HOL/Tools/res_atp.ML Thu Apr 19 16:38:59 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML Thu Apr 19 18:23:11 2007 +0200
@@ -718,7 +718,7 @@
(*Called by the oracle-based methods declared in res_atp_methods.ML*)
fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
let val conj_cls = make_clauses conjectures
- |> ResAxioms.assume_abstract_list true |> Meson.finish_cnf
+ |> ResAxioms.assume_abstract_list "subgoal" |> Meson.finish_cnf
val hyp_cls = cnf_hyps_thms ctxt
val goal_cls = conj_cls@hyp_cls
val goal_tms = map prop_of goal_cls