src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 15787 8fad4bd4e53c
parent 15782 a1863ea9052b
child 15789 4cb16144c81b
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Apr 20 22:43:52 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Apr 21 10:05:06 2005 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  (* Versions that include type information *)
     1.5   
     1.6  fun string_of_thm thm = let val _ = set show_sorts
     1.7 -                                val str = string_of_thm thm
     1.8 +                                val str = Display.string_of_thm thm
     1.9                                  val no_returns =List.filter not_newline (explode str)
    1.10                                  val _ = reset show_sorts
    1.11                              in 
    1.12 @@ -222,9 +222,6 @@
    1.13                                              (distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas)))
    1.14                                           end
    1.15                                          
    1.16 -fun thmstrings [] str = str
    1.17 -|   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
    1.18 -
    1.19  fun numclstr (vars, []) str = str
    1.20  |   numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
    1.21                                 in