--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Apr 21 13:15:25 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Apr 21 15:05:24 2005 +0200
@@ -1,3 +1,8 @@
+(* ID: $Id$
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
+*)
+
(******************)
(* complete later *)
(******************)
@@ -23,15 +28,6 @@
end
-fun thm_of_string str = let val _ = set show_sorts
- val term = read str
- val propterm = HOLogic.mk_Trueprop term
- val cterm = cterm_of Mainsign propterm
- val _ = reset show_sorts
- in
- assume cterm
- end
-
(* check separate args in the watcher program for separating strings with a * or ; or something *)
fun clause_strs_to_string [] str = str