src/HOL/Tools/res_atp.ML
changeset 20419 df257a9cf0e9
parent 20372 e42674e0486e
child 20423 593053389701
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Aug 25 18:48:09 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Aug 25 18:48:58 2006 +0200
     1.3 @@ -63,7 +63,7 @@
     1.4  (*** background linkup ***)
     1.5  val call_atp = ref false; 
     1.6  val hook_count = ref 0;
     1.7 -val time_limit = ref 30;
     1.8 +val time_limit = ref 80;
     1.9  val prover = ref "E";   (* use E as the default prover *)
    1.10  val custom_spass =   (*specialized options for SPASS*)
    1.11        ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"];
    1.12 @@ -735,7 +735,7 @@
    1.13  	      let val st = Seq.hd (EVERY' [rtac ccontr, ObjectLogic.atomize_tac, 
    1.14  	                                   skolemize_tac] n th)
    1.15  		  val negs = Option.valOf (metahyps_thms n st)
    1.16 -		  val negs_clauses = make_clauses negs
    1.17 +		  val negs_clauses = ResAxioms.assume_abstract (make_clauses negs)
    1.18  	      in
    1.19  		  negs_clauses :: get_neg_subgoals (n-1)
    1.20  	      end
    1.21 @@ -809,7 +809,7 @@
    1.22  		  Pretty.string_of (ProofContext.pretty_term ctxt
    1.23  		    (Logic.mk_conjunction_list (Thm.prems_of goal))));
    1.24      Output.debug ("current theory: " ^ Context.theory_name thy);
    1.25 -    hook_count := !hook_count +1;
    1.26 +    inc hook_count;
    1.27      Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
    1.28      ResClause.init thy;
    1.29      ResHolClause.init thy;