TFL/thry.sml

--- a/TFL/thry.sml	Mon May 26 12:28:30 1997 +0200
+++ b/TFL/thry.sml	Mon May 26 12:29:10 1997 +0200
@@ -64,7 +64,7 @@
 in
 fun make_definition parent s tm = 
    let val {lhs,rhs} = S.dest_eq tm
-       val {Name,Ty} = S.dest_var lhs
+       val (Name,Ty) = dest_Free lhs
        val lhs1 = S.mk_const{Name = Name, Ty = Ty}
        val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop}
        val dtm = list_comb(eeq1,[lhs1,rhs])      (* Rename "=" to "==" *)