src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 16803 014090d1e64b
parent 16548 aa36ae6b955e
child 16905 fa26952fa7b6
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Jul 13 16:07:23 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Jul 13 16:07:24 2005 +0200
     1.3 @@ -9,11 +9,11 @@
     1.4  
     1.5  structure Recon_Transfer =
     1.6  struct
     1.7 +
     1.8  open Recon_Parse
     1.9 +
    1.10  infixr 8 ++; infixr 7 >>; infixr 6 ||;
    1.11  
    1.12 -fun not_newline ch = not (ch = "\n");
    1.13 -
    1.14  
    1.15  
    1.16  (*
    1.17 @@ -51,14 +51,9 @@
    1.18  
    1.19  (* Versions that include type information *)
    1.20   
    1.21 +(* FIXME rename to str_of_thm *)
    1.22  fun string_of_thm thm =
    1.23 -  let val _ = set show_sorts
    1.24 -      val str = Display.string_of_thm thm
    1.25 -      val no_returns =List.filter not_newline (explode str)
    1.26 -      val _ = reset show_sorts
    1.27 -  in 
    1.28 -      implode no_returns
    1.29 -  end
    1.30 +  setmp show_sorts true (Pretty.str_of o Display.pretty_thm) thm;
    1.31  
    1.32  
    1.33  (* check separate args in the watcher program for separating strings with a * or ; or something *)
    1.34 @@ -377,31 +372,16 @@
    1.35  \1453[0:Rew:1279.0,1430.0,1242.0,1430.0,1279.0,1430.0] || equal(const_0,const_0)* -> .\
    1.36  \1454[0:Obv:1453.0] ||  -> .";*)
    1.37  
    1.38 -fun remove_linebreaks str = let val strlist = explode str
    1.39 -	                        val nonewlines = filter (not_equal "\n") strlist
    1.40 -	                    in
    1.41 -				implode nonewlines
    1.42 -			    end
    1.43 -
    1.44 +fun subst_for a b [] = ""
    1.45 +  | subst_for a b (x :: xs) =
    1.46 +      if x = a
    1.47 +      then 
    1.48 +	b ^ subst_for a b xs
    1.49 +      else
    1.50 +	x ^ subst_for a b xs;
    1.51  
    1.52 -fun subst_for a b [] = ""
    1.53 -|   subst_for a b (x::xs) = if (x = a)
    1.54 -				   then 
    1.55 -					(b^(subst_for a b  xs))
    1.56 -				   else
    1.57 -					x^(subst_for a b xs)
    1.58 -
    1.59 -
    1.60 -fun remove_linebreaks str = let val strlist = explode str
    1.61 -			    in
    1.62 -				subst_for "\n" "\t" strlist
    1.63 -			    end
    1.64 -
    1.65 -fun restore_linebreaks str = let val strlist = explode str
    1.66 -			     in
    1.67 -				subst_for "\t" "\n" strlist
    1.68 -			     end
    1.69 -
    1.70 +val remove_linebreaks = subst_for "\n" "\t" o explode;
    1.71 +val restore_linebreaks = subst_for "\t" "\n" o explode;
    1.72  
    1.73  
    1.74  fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  =