equal
deleted
inserted
replaced
80 val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
80 val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
81 val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |
81 val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |
82 val _ = if is_Const rhs then () else warning "The definiens is not a constant" |
82 val _ = if is_Const rhs then () else warning "The definiens is not a constant" |
83 |
83 |
84 in |
84 in |
85 Quotient_Def.add_quotient_def (((binding, mx), Attrib.empty_binding), (lhs, rhs)) rsp_thm ctxt |
85 Quotient_Def.add_quotient_def (((binding, mx), Binding.empty_atts), (lhs, rhs)) rsp_thm ctxt |
86 end |
86 end |
87 |
87 |
88 |
88 |
89 (* defines quotient constants *) |
89 (* defines quotient constants *) |
90 fun define_qconsts qtys consts_specs lthy = |
90 fun define_qconsts qtys consts_specs lthy = |