57 val Const(eeq_name, ty) = eeq |
57 val Const(eeq_name, ty) = eeq |
58 val prop = #2 (S.strip_type ty) |
58 val prop = #2 (S.strip_type ty) |
59 in |
59 in |
60 fun make_definition parent s tm = |
60 fun make_definition parent s tm = |
61 let val {lhs,rhs} = S.dest_eq tm |
61 let val {lhs,rhs} = S.dest_eq tm |
62 val (Name,Ty) = dest_Free lhs |
62 val (Name,Ty) = dest_Const lhs |
63 val lhs1 = S.mk_const{Name = Name, Ty = Ty} |
63 val lhs1 = S.mk_const{Name = Name, Ty = Ty} |
64 val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop} |
64 val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop} |
65 val dtm = list_comb(eeq1,[lhs1,rhs]) (* Rename "=" to "==" *) |
65 val dtm = list_comb(eeq1,[lhs1,rhs]) (* Rename "=" to "==" *) |
66 val (_, tm', _) = Sign.infer_types (sign_of parent) |
66 val (_, tm', _) = Sign.infer_types (sign_of parent) |
67 (K None) (K None) [] true ([dtm],propT) |
67 (K None) (K None) [] true ([dtm],propT) |