diff --git a/src/syntax/FStarC.Syntax.Util.fst b/src/syntax/FStarC.Syntax.Util.fst index bd7dc1d2627..cb30ec79834 100644 --- a/src/syntax/FStarC.Syntax.Util.fst +++ b/src/syntax/FStarC.Syntax.Util.fst @@ -1810,8 +1810,8 @@ let destruct_lemma_with_smt_patterns (t:term) Errors.raise_error p Errors.Error_IllSMTPat [ prefix 2 1 (text "Not an atomic SMT pattern:") (ttd p); - text "Patterns on lemmas must be a list of simple SMTPat's;\ - or a single SMTPatOr containing a list;\ + text "Patterns on lemmas must be a list of simple SMTPat's; \ + or a single SMTPatOr containing a list \ of lists of patterns." ] in