# HG changeset patch
# User wenzelm
# Date 955667691 -7200
# Node ID cbc02c7d82297bf4bcc5b48923ce2d8235b25859
# Parent  00ec2ba9174d697a26a5e2aec6efd4da543d3ac5
use HOLogic.termT;

diff -r 00ec2ba9174d -r cbc02c7d8229 TFL/post.sml
--- a/TFL/post.sml	Thu Apr 13 17:49:42 2000 +0200
+++ b/TFL/post.sml	Fri Apr 14 01:14:51 2000 +0200
@@ -184,7 +184,6 @@
  (*Strip off the outer !P*)
  val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
 
- (*this function could be combined with define_i --lcp*)
  fun simplify_defn (ss, tflCongs) (thy,(id,pats)) =
     let val dummy = deny (id mem (Sign.stamp_names_of (Theory.sign_of thy)))
 			 ("Recursive definition " ^ id ^ 
@@ -222,7 +221,7 @@
 
  fun define thy fid R ss_congs seqs = 
    let val _ =  writeln ("Recursive function " ^ fid)
-       val read = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[])) 
+       val read = readtm (Theory.sign_of thy) HOLogic.termT;
    in  define_i thy fid (read R) ss_congs (map read seqs)  end
    handle Utils.ERR {mesg,...} => error mesg;
 
@@ -255,7 +254,7 @@
   end
 
  fun defer thy fid congs seqs = 
-   let val read = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[]))
+   let val read = readtm (Theory.sign_of thy) HOLogic.termT;
    in  defer_i thy fid congs (map read seqs)  end
    handle Utils.ERR {mesg,...} => error mesg;
  end;