--- a/TFL/post.ML Mon Aug 01 19:20:28 2005 +0200
+++ b/TFL/post.ML Mon Aug 01 19:20:29 2005 +0200
@@ -37,9 +37,6 @@
(* misc *)
-val read_term = Thm.term_of oo (HOLogic.read_cterm o Theory.sign_of);
-
-
(*---------------------------------------------------------------------------
* Extract termination goals so that they can be put it into a goalstack, or
* have a tactic directly applied to them.
@@ -248,7 +245,7 @@
in (thy, {rules = rules', induct = induct, tcs = tcs}) end;
fun define strict thy cs ss congs wfs fid R seqs =
- define_i strict thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs)
+ define_i strict thy cs ss congs wfs fid (Sign.read_term thy R) (map (Sign.read_term thy) seqs)
handle U.ERR {mesg,...} => error mesg;
@@ -275,7 +272,7 @@
end
fun defer thy congs fid seqs =
- defer_i thy congs fid (map (read_term thy) seqs)
+ defer_i thy congs fid (map (Sign.read_term thy) seqs)
handle U.ERR {mesg,...} => error mesg;
end;