TFL/post.ML

--- a/TFL/post.ML	Tue Jun 13 23:41:37 2006 +0200
+++ b/TFL/post.ML	Tue Jun 13 23:41:39 2006 +0200
@@ -170,7 +170,7 @@
   | tracing false msg = writeln msg;
 
 fun simplify_defn strict thy cs ss congs wfs id pats def0 =
-   let val def = freezeT def0 RS meta_eq_to_obj_eq
+   let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
        val {theory,rules,rows,TCs,full_pats_TCs} =
            Prim.post_definition congs (thy, (def,pats))
        val {lhs=f,rhs} = S.dest_eq (concl def)