diff options
| author | Thomas Bauereiss | 2018-02-16 20:04:17 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-02-16 20:04:17 +0000 |
| commit | 6bd490a9a3570fbb6f8a5979aaf4cd3ada3131d1 (patch) | |
| tree | 8eba710a5ade024e695b3062bafe8d2c15ba12fc /src/pretty_print_lem.ml | |
| parent | 18767e96381dc5fdd5a88fc18a355b5f67433021 (diff) | |
Avoid nested explicit type annotations
Isabelle does not like nested annotations like "((exp :: typ) :: typ)".
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 730cf4a8..38862382 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -449,8 +449,8 @@ let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with | P_typ(Typ_aux (Typ_tup typs, _), P_aux (P_tup pats, _)) -> (* Isabelle does not seem to like type-annotated tuple patterns; it gives a syntax error. Avoid this by annotating the tuple elements instead *) - let doc_elem typ (P_aux (_, annot) as pat) = - doc_pat_lem ctxt true (P_aux (P_typ (typ, pat), annot)) in + let doc_elem typ pat = + doc_pat_lem ctxt true (add_p_typ typ pat) in parens (separate comma_sp (List.map2 doc_elem typs pats)) | P_typ(typ,p) -> let doc_p = doc_pat_lem ctxt true p in |