TFL/thry.sml

--- a/TFL/thry.sml	Mon Jun 02 12:17:19 1997 +0200
+++ b/TFL/thry.sml	Mon Jun 02 12:19:01 1997 +0200
@@ -59,7 +59,7 @@
 in
 fun make_definition parent s tm = 
    let val {lhs,rhs} = S.dest_eq tm
-       val (Name,Ty) = dest_Free lhs
+       val (Name,Ty) = dest_Const 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 "==" *)