diff --git a/src/parser/ast_term.ml b/src/parser/ast_term.ml
index 63e40f05..bbc84638 100644
--- a/src/parser/ast_term.ml
+++ b/src/parser/ast_term.ml
@@ -179,8 +179,8 @@ let rec pp_proof out (p : proof) : unit =
 
 and pp_proof_step out (step : proof_step) : unit =
   let s = step.view in
-  Fmt.fprintf out "@[<2>have %s := %a@ proof %a@]" s.name pp_term s.goal
-    pp_proof s.proof
+  Fmt.fprintf out "@[<2>have %s := %a@ %a@]" s.name pp_term s.goal pp_proof
+    s.proof
 
 let pp_decl out (d : decl) =
   match d.view with
@@ -195,5 +195,5 @@ let pp_decl out (d : decl) =
       args pp_tyret () pp_term rhs
   | D_hash (name, t) -> Fmt.fprintf out "@[<2>#%s@ %a@];" name pp_term t
   | D_theorem { name; goal; proof } ->
-    Fmt.fprintf out "@[<hv2>theorem %s :=@ %a@ @[<hv2>proof %a@]@];" name
-      pp_term goal pp_proof proof
+    Fmt.fprintf out "@[<hv2>theorem %s :=@ %a@ @[<hv>%a@]@];" name pp_term goal
+      pp_proof proof
diff --git a/src/parser/lex.mll b/src/parser/lex.mll
index be33a831..fba89f20 100644
--- a/src/parser/lex.mll
+++ b/src/parser/lex.mll
@@ -24,6 +24,8 @@ rule token = parse
 | ":" { COLON }
 | "(" { LPAREN }
 | ")" { RPAREN }
+| "{" { LBRACE }
+| "}" { RBRACE }
 | ":=" { EQDEF }
 | "->" { ARROW }
 | "." { DOT }
diff --git a/src/parser/parse_util.ml b/src/parser/parse_util.ml
index 23b1a7a7..89bfd6fd 100644
--- a/src/parser/parse_util.ml
+++ b/src/parser/parse_util.ml
@@ -8,6 +8,11 @@ module Error = struct
   let pp out (self : t) =
     Fmt.fprintf out "parse error: %s@ %a" self.msg Loc.pp self.loc
 
+  let pp_with_loc ~input out (self : t) =
+    Fmt.fprintf out "parse error: %s@ %a" self.msg
+      (Loc.pp_loc ~max_lines:5 ~input)
+      [ self.loc ]
+
   let to_string = Fmt.to_string pp
 end