src/HOL/Tools/res_atp.ML
changeset 16925 0fd7b1438d28
parent 16904 6fb188ca5f91
child 16955 93270c5f56f6
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Jul 27 11:28:18 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Jul 27 11:30:34 2005 +0200
     1.3 @@ -90,6 +90,8 @@
     1.4  (* a special version of repeat_RS *)
     1.5  fun repeat_someI_ex thm = repeat_RS thm someI_ex;
     1.6  
     1.7 +
     1.8 +(*FIXME: is function isar_atp_h used? If not, delete!*)
     1.9  (*********************************************************************)
    1.10  (* convert clauses from "assume" to conjecture. write to file "hyps" *)
    1.11  (* hypotheses of the goal currently being proved                     *)
    1.12 @@ -383,7 +385,7 @@
    1.13      debug ("initial thm in isar_atp: " ^ string_of_thm goal);
    1.14      debug ("subgoals in isar_atp: " ^ prems_string);
    1.15      debug ("number of subgoals in isar_atp: " ^ string_of_int (Thm.nprems_of goal));
    1.16 -    (*isar_local_thms (d_cs,d_ss_thms);*)
    1.17 +    ResClause.init thy;
    1.18      isar_atp' (ctxt, ProofContext.prems_of ctxt, goal)
    1.19    end);
    1.20