equal
deleted
inserted
replaced
170 error_at ctxt ats ("Unexpected recursive call in " ^ quote (Syntax.string_of_term ctxt t)); |
170 error_at ctxt ats ("Unexpected recursive call in " ^ quote (Syntax.string_of_term ctxt t)); |
171 fun unexpected_corec_call_in ctxt ats t = |
171 fun unexpected_corec_call_in ctxt ats t = |
172 error_at ctxt ats ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t)); |
172 error_at ctxt ats ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t)); |
173 fun unsupported_case_around_corec_call ctxt ats t = |
173 fun unsupported_case_around_corec_call ctxt ats t = |
174 error_at ctxt ats ("Unsupported corecursive call under case expression " ^ |
174 error_at ctxt ats ("Unsupported corecursive call under case expression " ^ |
175 quote (Syntax.string_of_term ctxt t) ^ "\n(Define " ^ |
175 quote (Syntax.string_of_term ctxt t) ^ |
176 quote (Syntax.string_of_typ ctxt (domain_type (fastype_of t))) ^ |
176 "\n(Define datatype with discriminators and selectors to circumvent this limitation)"); |
177 " with discriminators and selectors to circumvent this limitation)"); |
|
178 |
177 |
179 fun no_equation_for_ctr_warning ctxt ats ctr = |
178 fun no_equation_for_ctr_warning ctxt ats ctr = |
180 warning_at ctxt ats ("No equation for constructor " ^ quote (Syntax.string_of_term ctxt ctr)); |
179 warning_at ctxt ats ("No equation for constructor " ^ quote (Syntax.string_of_term ctxt ctr)); |
181 |
180 |
182 fun check_all_fun_arg_frees ctxt ats fun_args = |
181 fun check_all_fun_arg_frees ctxt ats fun_args = |