src/HOL/Tools/res_atp.ML
changeset 15736 1bb0399a9517
parent 15700 970e0293dfb3
child 15774 9df37a0e935d
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Apr 15 12:00:00 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Apr 15 13:35:53 2005 +0200
     1.3 @@ -64,12 +64,6 @@
     1.4  val dummy_tac = PRIMITIVE(fn thm => thm );
     1.5  
     1.6   
     1.7 -fun concat_with_and [] str = str
     1.8 -|   concat_with_and (x::[]) str = str^" ("^x^")"
     1.9 -|   concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & "))
    1.10 -
    1.11 -
    1.12 -
    1.13  (**** for Isabelle/ML interface  ****)
    1.14  
    1.15  fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ")
    1.16 @@ -147,7 +141,7 @@
    1.17  (*********************************************************************)
    1.18  
    1.19  fun call_resolve_tac sign thms sg_term (childin, childout,pid) n  = let
    1.20 -                             val thmstring = concat_with_and (map string_of_thm thms) ""
    1.21 +                             val thmstring = Meson.concat_with_and (map string_of_thm thms)
    1.22                               val thm_no = length thms
    1.23                               val _ = warning ("number of thms is : "^(string_of_int thm_no))
    1.24                               val _ = warning ("thmstring in call_res is: "^thmstring)
    1.25 @@ -163,7 +157,7 @@
    1.26                               val clauses = make_clauses thms
    1.27                               val _ =( warning ("called make_clauses "))*)
    1.28                               (*val _ = tptp_inputs clauses prob_file*)
    1.29 -                             val thmstring = concat_with_and (map string_of_thm thms) ""
    1.30 +                             val thmstring = Meson.concat_with_and (map string_of_thm thms)
    1.31                             
    1.32                               val goalstr = Sign.string_of_term sign sg_term 
    1.33                               val goalproofstring = proofstring goalstr
    1.34 @@ -227,7 +221,8 @@
    1.35  (* dummy tac vs.  Doesn't call resolve_tac *)
    1.36  
    1.37  fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) = 
    1.38 -                                         ( warning("ths for tptp: " ^ (concat_with_and (map string_of_thm thms) ""));
    1.39 +                                         ( warning("ths for tptp: " ^ 
    1.40 +                                                   Meson.concat_with_and (map string_of_thm thms));
    1.41                                             warning("in call_atp_tac_tfrees");
    1.42                                             
    1.43                                             tptp_inputs_tfrees (make_clauses thms) n tfrees;
    1.44 @@ -243,7 +238,7 @@
    1.45  SELECT_GOAL
    1.46    (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    1.47    METAHYPS(fn negs => (warning("calling  call_atp_tac_tfrees with negs"
    1.48 -                               ^ (concat_with_and (map string_of_thm negs) ""));
    1.49 +                               ^ Meson.concat_with_and (map string_of_thm negs));
    1.50             call_atp_tac_tfrees sign negs n tfrees sg_term (childin, childout,pid) ))]) n st
    1.51  end;
    1.52  
    1.53 @@ -305,9 +300,9 @@
    1.54          val _= (warning ("in isar_atp'"))
    1.55          val prems = prems_of thm
    1.56          val sign = sign_of_thm thm
    1.57 -        val thms_string =concat_with_and (map  string_of_thm thms) ""
    1.58 +        val thms_string = Meson.concat_with_and (map string_of_thm thms)
    1.59          val thmstring = string_of_thm thm
    1.60 -        val prems_string = concat_with_and (map (Sign.string_of_term sign) prems) ""
    1.61 +        val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
    1.62          (* set up variables for writing out the clasimps to a tptp file *)
    1.63          val _ = write_out_clasimp (File.sysify_path axiom_file)
    1.64          (* cq: add write out clasimps to file *)
    1.65 @@ -397,9 +392,8 @@
    1.66          val sg_prems = prems_of thm
    1.67          val sign = sign_of_thm thm
    1.68          val prem_no = length sg_prems
    1.69 -        val prems_string =  concat_with_and (map (Sign.string_of_term sign) sg_prems) ""
    1.70 +        val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems)
    1.71      in
    1.72 -         
    1.73            (warning ("initial thm in isar_atp: "^thmstring));
    1.74            (warning ("subgoals in isar_atp: "^prems_string));
    1.75      	   (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));