src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 15700 970e0293dfb3
parent 15697 681bcb7f0389
child 15739 bb2acfed8212
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Apr 12 11:07:42 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Apr 12 11:08:25 2005 +0200
     1.3 @@ -149,8 +149,8 @@
     1.4                                        add_if_not_inlist ys xs (y::newlist)
     1.5                                          else add_if_not_inlist ys xs (newlist)
     1.6  
     1.7 -fun onestr [] str = str
     1.8 -|   onestr (x::xs) str = onestr xs (str^(concat x))
     1.9 +(*Flattens a list of list of strings to one string*)
    1.10 +fun onestr ls = String.concat (map String.concat ls);
    1.11  
    1.12  fun thmstrings [] str = str
    1.13  |   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
    1.14 @@ -159,11 +159,6 @@
    1.15  |   onelist (x::xs) newlist = onelist xs (newlist@x)
    1.16  
    1.17  
    1.18 -
    1.19 -val prop_of = #prop o rep_thm;
    1.20 -
    1.21 -
    1.22 -
    1.23   fun get_axioms_used proof_steps thmstring = let 
    1.24                                               val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
    1.25                                               val _ = TextIO.output (outfile, thmstring)
    1.26 @@ -194,11 +189,11 @@
    1.27                                             
    1.28                                              val metas_and_strs = zip  metas meta_strs
    1.29                                               val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));                                                                       
    1.30 -                                             val _ = TextIO.output (outfile, (onestr ax_strs ""))
    1.31 +                                             val _ = TextIO.output (outfile, onestr ax_strs)
    1.32                                               
    1.33                                               val _ =  TextIO.closeOut outfile
    1.34                                               val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metastrs")));                                                                       
    1.35 -                                             val _ = TextIO.output (outfile, (onestr meta_strs ""))
    1.36 +                                             val _ = TextIO.output (outfile, onestr meta_strs)
    1.37                                               val _ =  TextIO.closeOut outfile
    1.38  
    1.39                                              (* get list of axioms as thms with their variables *)