removed bad code
authorpaulson
Thu Apr 07 18:44:45 2005 +0200 (2005-04-07)
changeset 1568209a7b8909c4d
parent 15681 b667c22edb36
child 15683 196f40d3ffea
removed bad code
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Apr 07 18:35:21 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Apr 07 18:44:45 2005 +0200
     1.3 @@ -8,8 +8,6 @@
     1.4  (*Jia: changed: isar_atp now processes entire proof context.  fetch thms from delta simpset/claset*)
     1.5  (*Claire: changed: added actual watcher calls *)
     1.6  
     1.7 -val traceflag = ref true;
     1.8 -
     1.9  signature RES_ATP = 
    1.10  sig
    1.11  val trace_res : bool ref
    1.12 @@ -256,7 +254,7 @@
    1.13     
    1.14     in
    1.15  SELECT_GOAL
    1.16 -  (EVERY1 [rtac ccontr,atomize_tac, tracify traceflag skolemize_tac, 
    1.17 +  (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    1.18    METAHYPS(fn negs => ((warning("calling  call_atp_tac_tfrees with negs"^(concat_with_and (map  string_of_thm negs) "")));call_atp_tac_tfrees (negs) n tfrees sg_term (childin, childout,pid) ))]) n
    1.19  end;
    1.20