src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 15789 4cb16144c81b
parent 15787 8fad4bd4e53c
child 15817 f79b673da664
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Apr 21 13:15:25 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Apr 21 15:05:24 2005 +0200
     1.3 @@ -1,3 +1,8 @@
     1.4 +(*  ID:         $Id$
     1.5 +    Author:     Claire Quigley
     1.6 +    Copyright   2004  University of Cambridge
     1.7 +*)
     1.8 +
     1.9  (******************)
    1.10  (* complete later *)
    1.11  (******************)
    1.12 @@ -23,15 +28,6 @@
    1.13                              end
    1.14  
    1.15  
    1.16 -fun thm_of_string str = let val _ = set show_sorts
    1.17 -                                val term = read str
    1.18 -                                val propterm = HOLogic.mk_Trueprop term
    1.19 -                                val cterm = cterm_of Mainsign propterm
    1.20 -                                val _ = reset show_sorts
    1.21 -                            in
    1.22 -                                assume cterm
    1.23 -                            end
    1.24 -
    1.25  (* check separate args in the watcher program for separating strings with a * or ; or something *)
    1.26  
    1.27  fun clause_strs_to_string [] str = str