equal
deleted
inserted
replaced
129 error_at ctxt eqns "Nonprimitive corecursive specification"; |
129 error_at ctxt eqns "Nonprimitive corecursive specification"; |
130 fun unexpected_corec_call ctxt eqns t = |
130 fun unexpected_corec_call ctxt eqns t = |
131 error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t)); |
131 error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t)); |
132 fun unsupported_case_around_corec_call ctxt eqns t = |
132 fun unsupported_case_around_corec_call ctxt eqns t = |
133 error_at ctxt eqns ("Unsupported corecursive call under case expression " ^ |
133 error_at ctxt eqns ("Unsupported corecursive call under case expression " ^ |
134 quote (Syntax.string_of_term ctxt t) ^ "\n(Define " ^ |
134 quote (Syntax.string_of_term ctxt t) ^ " for datatype with no discriminators and selectors"); |
135 quote (Syntax.string_of_typ ctxt (domain_type (fastype_of t))) ^ |
|
136 " with discriminators and selectors to circumvent this limitation.)"); |
|
137 fun use_primcorecursive () = |
135 fun use_primcorecursive () = |
138 error ("\"auto\" failed (try " ^ quote (#1 @{command_keyword primcorecursive}) ^ " instead of " ^ |
136 error ("\"auto\" failed (try " ^ quote (#1 @{command_keyword primcorecursive}) ^ " instead of " ^ |
139 quote (#1 @{command_keyword primcorec}) ^ ")"); |
137 quote (#1 @{command_keyword primcorec}) ^ ")"); |
140 |
138 |
141 datatype corec_option = |
139 datatype corec_option = |