TFL/thry.sml
changeset 3332 3921ebbd9cf0
parent 3302 404fe31fd8d2
child 3353 9112a2efb9a3
     1.1 --- a/TFL/thry.sml	Mon May 26 12:28:30 1997 +0200
     1.2 +++ b/TFL/thry.sml	Mon May 26 12:29:10 1997 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4  in
     1.5  fun make_definition parent s tm = 
     1.6     let val {lhs,rhs} = S.dest_eq tm
     1.7 -       val {Name,Ty} = S.dest_var lhs
     1.8 +       val (Name,Ty) = dest_Free lhs
     1.9         val lhs1 = S.mk_const{Name = Name, Ty = Ty}
    1.10         val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop}
    1.11         val dtm = list_comb(eeq1,[lhs1,rhs])      (* Rename "=" to "==" *)