--- a/src/HOL/Tools/res_atp.ML Wed Jul 27 11:28:18 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Wed Jul 27 11:30:34 2005 +0200
@@ -90,6 +90,8 @@
(* a special version of repeat_RS *)
fun repeat_someI_ex thm = repeat_RS thm someI_ex;
+
+(*FIXME: is function isar_atp_h used? If not, delete!*)
(*********************************************************************)
(* convert clauses from "assume" to conjecture. write to file "hyps" *)
(* hypotheses of the goal currently being proved *)
@@ -383,7 +385,7 @@
debug ("initial thm in isar_atp: " ^ string_of_thm goal);
debug ("subgoals in isar_atp: " ^ prems_string);
debug ("number of subgoals in isar_atp: " ^ string_of_int (Thm.nprems_of goal));
- (*isar_local_thms (d_cs,d_ss_thms);*)
+ ResClause.init thy;
isar_atp' (ctxt, ProofContext.prems_of ctxt, goal)
end);