diff --git a/intTests/test_parse_errors/coreparser001.log.good b/intTests/test_parse_errors/coreparser001.log.good
new file mode 100644
index 000000000..d48ba035b
--- /dev/null
+++ b/intTests/test_parse_errors/coreparser001.log.good
@@ -0,0 +1,7 @@
+ Loading file "coreparser001.saw"
+ Stack trace:
+"load_sawcore_from_file" (coreparser001.saw:2:1-2:23)
+Module parsing failed:
+PosPair {_pos = Pos {posBase = ".", posPath = "coreparser001.sawcore", posLine = 2, posCol = 7}, val = UnexpectedToken (TKey "where")}
+
+FAILED
diff --git a/intTests/test_parse_errors/coreparser001.saw b/intTests/test_parse_errors/coreparser001.saw
new file mode 100644
index 000000000..13a09bfd4
--- /dev/null
+++ b/intTests/test_parse_errors/coreparser001.saw
@@ -0,0 +1,2 @@
+enable_experimental;
+load_sawcore_from_file "coreparser001.sawcore";
diff --git a/intTests/test_parse_errors/coreparser001.sawcore b/intTests/test_parse_errors/coreparser001.sawcore
new file mode 100644
index 000000000..457f6d5d2
--- /dev/null
+++ b/intTests/test_parse_errors/coreparser001.sawcore
@@ -0,0 +1,3 @@
+-- Missing module name in file header
+module where
+import Prelude;
diff --git a/saw-core/src/SAWCore/Grammar.y b/saw-core/src/SAWCore/Grammar.y
index 817bbf2ff..8d36681ba 100644
--- a/saw-core/src/SAWCore/Grammar.y
+++ b/saw-core/src/SAWCore/Grammar.y
@@ -1,5 +1,6 @@
 {
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -fno-warn-tabs #-}
 
@@ -33,12 +34,16 @@ import System.Directory (getCurrentDirectory)
 
 import Prelude hiding (mapM, sequence)
 
+import SAWCore.Panic
 import SAWCore.UntypedAST
 import SAWCore.Module (DefQualifier(..))
 import SAWCore.Lexer
 
 }
 
+-- edit width for this file is 100:
+----------------------------------------------------------------------------------------------------
+
 %name parseSAW2 Module
 %name parseSAWTerm2 Term
 
@@ -49,205 +54,222 @@ import SAWCore.Lexer
 %expect 0
 
 %token
-  '#'     { PosPair _ (TKey "#") }
-  '->'    { PosPair _ (TKey "->") }
-  '='     { PosPair _ (TKey "=") }
-  '\\'    { PosPair _ (TKey "\\") }
-  ';'     { PosPair _ (TKey ";") }
-  ':'     { PosPair _ (TKey ":") }
-  ','     { PosPair _ (TKey ",") }
-  '.'     { PosPair _ (TKey ".") }
-  '('     { PosPair _ (TKey "(") }
-  ')'     { PosPair _ (TKey ")") }
-  '['     { PosPair _ (TKey "[") }
-  ']'     { PosPair _ (TKey "]") }
-  '{'     { PosPair _ (TKey "{") }
-  '}'     { PosPair _ (TKey "}") }
-  '|'     { PosPair _ (TKey "|") }
-  '*'     { PosPair _ (TKey "*") }
-  'data'      { PosPair _ (TKey "data") }
-  'hiding'    { PosPair _ (TKey "hiding") }
-  'import'    { PosPair _ (TKey "import") }
-  'module'    { PosPair _ (TKey "module") }
-  'sort'      { PosPair _ (TKey "sort") }
-  'isort'     { PosPair _ (TKey "isort") }
-  'qsort'     { PosPair _ (TKey "qsort") }
-  'qisort'    { PosPair _ (TKey "qisort") }
-  'Prop'      { PosPair _ (TKey "Prop") }
-  'where'     { PosPair _ (TKey "where") }
-  'axiom'     { PosPair _ (TKey "axiom") }
-  'primitive' { PosPair _ (TKey "primitive") }
-  'injectCode' { PosPair _ (TKey "injectCode") }
-
-  nat      { PosPair _ (TNat _) }
-  bvlit    { PosPair _ (TBitvector _) }
-  '_'      { PosPair _ (TIdent "_") }
-  ident    { PosPair _ (TIdent _) }
-  identrec { PosPair _ (TRecursor _) }
-  string   { PosPair _ (TString _) }
+  '#'           { PosPair _ (TKey "#") }
+  '->'          { PosPair _ (TKey "->") }
+  '='           { PosPair _ (TKey "=") }
+  '\\'          { PosPair _ (TKey "\\") }
+  ';'           { PosPair _ (TKey ";") }
+  ':'           { PosPair _ (TKey ":") }
+  ','           { PosPair _ (TKey ",") }
+  '.'           { PosPair _ (TKey ".") }
+  '('           { PosPair _ (TKey "(") }
+  ')'           { PosPair _ (TKey ")") }
+  '['           { PosPair _ (TKey "[") }
+  ']'           { PosPair _ (TKey "]") }
+  '{'           { PosPair _ (TKey "{") }
+  '}'           { PosPair _ (TKey "}") }
+  '|'           { PosPair _ (TKey "|") }
+  '*'           { PosPair _ (TKey "*") }
+  'data'        { PosPair _ (TKey "data") }
+  'hiding'      { PosPair _ (TKey "hiding") }
+  'import'      { PosPair _ (TKey "import") }
+  'module'      { PosPair _ (TKey "module") }
+  'sort'        { PosPair _ (TKey "sort") }
+  'isort'       { PosPair _ (TKey "isort") }
+  'qsort'       { PosPair _ (TKey "qsort") }
+  'qisort'      { PosPair _ (TKey "qisort") }
+  'Prop'        { PosPair _ (TKey "Prop") }
+  'where'       { PosPair _ (TKey "where") }
+  'axiom'       { PosPair _ (TKey "axiom") }
+  'primitive'   { PosPair _ (TKey "primitive") }
+  'injectCode'  { PosPair _ (TKey "injectCode") }
+
+  nat           { PosPair _ (TNat _) }
+  bvlit         { PosPair _ (TBitvector _) }
+  '_'           { PosPair _ (TIdent "_") }
+  rawident      { PosPair _ (TIdent _) }
+  rawidentrec   { PosPair _ (TRecursor _) }
+  string        { PosPair _ (TString _) }
 
 %%
 
-Module :: { Module }
-Module : 'module' ModuleName 'where' list(Import) list(SAWDecl) { Module $2 $4 $5 }
-
-ModuleName :: { PosPair ModuleName }
-ModuleName : sepBy (Ident, '.') { mkPosModuleName $1 }
-
-Import :: { Import }
-Import : 'import' ModuleName opt(ModuleImports) ';'
-          { Import $2 $3 }
-
-SAWDecl :: { Decl }
-SAWDecl : 'data' Ident VarCtx ':' LTerm 'where' '{' list(CtorDecl) '}'
-             { DataDecl $2 $3 $5 $8 }
-        | 'primitive' Ident ':' LTerm ';'
-             { TypeDecl PrimQualifier $2 $4 }
-        | 'axiom' Ident ':' LTerm ';'
-             { TypeDecl AxiomQualifier $2 $4 }
-        | Ident ':' LTerm opt(DefBody) ';' { maybe (TypeDecl NoQualifier $1 $3)
-                                                   (TypedDef $1 [] $3) $4 }
-        | Ident list(TermVar) '=' LTerm ';' { TermDef $1 $2 $4 }
-        | Ident VarCtxItem VarCtx ':' LTerm '=' LTerm ';' { TypedDef $1 ($2 ++ $3) $5 $7 }
-        | 'injectCode' string string ';'
-	     { InjectCodeDecl (Text.pack (tokString (val $2))) (Text.pack (tokString (val $3))) }
-
-DefBody :: { UTerm }
-DefBody : '=' LTerm { $2 }
-
-ModuleImports :: { ImportConstraint }
-ModuleImports : 'hiding' ImportNames { HidingImports $2 }
-              | ImportNames { SpecificImports $1 }
-
-ImportNames :: { [String] }
-ImportNames : '(' sepBy(ImportName, ',') ')' { $2 }
-
-ImportName :: { String }
-ImportName : ident { tokIdent $ val $1 }
-
-TermVar :: { UTermVar }
-TermVar
-  : Ident { TermVar $1 }
-  | '_' { UnusedVar (pos $1) }
-
--- A context of variables which may or may not be typed
-DefVarCtx :: { [(UTermVar, Maybe UTerm)] }
-DefVarCtx : list(DefVarCtxItem) { concat $1 }
-
-DefVarCtxItem :: { [(UTermVar, Maybe UTerm)] }
-DefVarCtxItem : TermVar { [($1, Nothing)] }
-              | '(' list(TermVar) ':'  LTerm ')'
-                { map (\var -> (var, Just $4)) $2 }
-
--- A context of variables, all of which must be typed; i.e., a list syntactic
--- elements of the form (x y z :: tp) (x2 y3 :: tp2) ...
-VarCtx :: { [(UTermVar, UTerm)] }
-VarCtx : list(VarCtxItem) { concat $1 }
-
-VarCtxItem :: { [(UTermVar, UTerm)] }
-VarCtxItem : '(' list(TermVar) ':' LTerm ')' { map (\var -> (var,$4)) $2 }
+-- whole module
+Module :: { Module } :
+  'module' ModuleName 'where' list(Import) list(SAWDecl)        { Module $2 $4 $5 }
+
+-- possibly-qualified module name
+ModuleName :: { PosPair ModuleName } :
+  sepBy1 (Ident, '.')                                           { mkPosModuleName $1 }
+
+-- import directive
+Import :: { Import } :
+  'import' ModuleName opt(ModuleImports) ';'                    { Import $2 $3 }
+
+-- top-level declaration
+SAWDecl :: { Decl } :
+    'data' Ident VarCtx ':' LTerm 'where' '{' list(CtorDecl) '}' { DataDecl $2 $3 $5 $8 }
+  | 'primitive' Ident ':' LTerm ';'                             { mkPrimitive $2 $4 }
+  | 'axiom' Ident ':' LTerm ';'                                 { mkAxiom $2 $4 }
+  | Ident ':' LTerm ';'                                         { mkNoQual $1 $3 }
+  | Ident ':' LTerm '=' LTerm ';'                               { TypedDef $1 [] $3 $5 }
+  | Ident list(TermVar) '=' LTerm ';'                           { TermDef $1 $2 $4 }
+  | Ident VarCtxItem VarCtx ':' LTerm '=' LTerm ';'             { TypedDef $1 ($2 ++ $3) $5 $7 }
+  | 'injectCode' string string ';'                              { mkInject $2 $3 }
+
+-- symbol import list in an import directive
+ModuleImports :: { ImportConstraint } :
+    'hiding' ImportNames                        { HidingImports $2 }
+  | ImportNames                                 { SpecificImports $1 }
+
+-- list of imported symbols
+ImportNames :: { [String] } :
+  '(' sepBy(ImportName, ',') ')'                { $2 }
+
+-- single imported symbol
+ImportName :: { String } :
+  rawident                                      { tokIdent $ val $1 }
+
+-- A single parameter
+TermVar :: { UTermVar } :
+    Ident                                       { TermVar $1 }
+  | '_'                                         { UnusedVar (pos $1) }
+
+-- A context of variables (parameter list) which may or may not be typed
+--
+-- XXX: this is unused. Is it intended that declarations can only have
+-- either all typed or all untyped parameters, or was it a hack to avoid
+-- some grammar problem that's probably fixable?
+DefVarCtx :: { [(UTermVar, Maybe UTerm)] } :
+  list(DefVarCtxItem)                           { concat $1 }
+
+-- Single entry in a parameter list: either a single variable or
+-- possibly several sharing a type. XXX: is it intended that the list
+-- can be empty?
+DefVarCtxItem :: { [(UTermVar, Maybe UTerm)] } :
+    TermVar                                     { [($1, Nothing)] }
+  | '(' list(TermVar) ':' LTerm ')'             { map (\var -> (var, Just $4)) $2 }
+
+-- A context of variables (parameter list), all of which must be
+-- typed; i.e., a list of syntactic elements of the form
+--    (x y z :: tp) (x2 y3 :: tp2) ...
+VarCtx :: { [(UTermVar, UTerm)] } :
+  list(VarCtxItem)                              { concat $1 }
+
+-- A single entry in a parameter list: several variables that share a type.
+-- XXX: is it intended that the list can be empty?
+VarCtxItem :: { [(UTermVar, UTerm)] } :
+  '(' list(TermVar) ':' LTerm ')'               { map (\var -> (var, $4)) $2 }
 
 -- Constructor declaration of the form "c (x1 x2 :: tp1) ... (z1 :: tpn) :: tp"
-CtorDecl :: { CtorDecl }
-CtorDecl : Ident VarCtx ':' LTerm ';' { Ctor $1 $2 $4 }
+CtorDecl :: { CtorDecl } :
+  Ident VarCtx ':' LTerm ';'                    { Ctor $1 $2 $4 }
 
-Term :: { UTerm }
-Term : LTerm { $1 }
-     | LTerm ':' LTerm { TypeConstraint $1 (pos $2) $3 }
+-- Full term (possibly including a type annotation)
+Term :: { UTerm } :
+    LTerm                                       { $1 }
+  | LTerm ':' LTerm                             { TypeConstraint $1 (pos $2) $3 }
 
 -- Term with uses of pi and lambda, but no type ascriptions
-LTerm :: { UTerm }
-LTerm : ProdTerm                         { $1 }
-      | PiArg '->' LTerm                 { Pi (pos $2) $1 $3 }
-      | '\\' VarCtx '->' LTerm           { Lambda (pos $1) $2 $4 }
-
-PiArg :: { [(UTermVar, UTerm)] }
-PiArg : ProdTerm { mkPiArg $1 }
+LTerm :: { UTerm } :
+    ProdTerm                                    { $1 }
+  | ProdTerm '->' LTerm                         { Pi (pos $2) (mkPiArg $1) $3 }
+  | '\\' VarCtx '->' LTerm                      { Lambda (pos $1) $2 $4 }
 
 -- Term formed from infix product type operator (right-associative)
-ProdTerm :: { UTerm }
-ProdTerm
-  : AppTerm                        { $1 }
-  | AppTerm '*' ProdTerm           { PairType (pos $1) $1 $3 }
+ProdTerm :: { UTerm } :
+    AppTerm                                     { $1 }
+  | AppTerm '*' ProdTerm                        { PairType (pos $1) $1 $3 }
 
 -- Term formed from applications of atomic expressions
-AppTerm :: { UTerm }
-AppTerm : AtomTerm                 { $1 }
-        | AppTerm AtomTerm         { App $1 $2 }
-
-AtomTerm :: { UTerm }
-AtomTerm
-  : nat                          { NatLit (pos $1) (tokNat (val $1)) }
-  | bvlit                        { BVLit (pos $1) (tokBits (val $1)) }
-  | string                       { StringLit (pos $1) (Text.pack (tokString (val $1))) }
-  | Ident                        { Name $1 }
-  | IdentRec                     { Recursor Nothing $1 }
-  | 'Prop'                       { Sort (pos $1) propSort noFlags }
-  | Sort nat                     { Sort (pos $1) (mkSort (tokNat (val $2))) (val $1) }
-  | AtomTerm '.' Ident           { RecordProj $1 (val $3) }
-  | AtomTerm '.' IdentRec        {% parseRecursorProj $1 $3 }
-  | AtomTerm '.' nat             {% parseTupleSelector $1 (fmap tokNat $3) }
-  | '(' sepBy(Term, ',') ')'     { mkTupleValue (pos $1) $2 }
-  | '#' '(' sepBy(Term, ',') ')'       { mkTupleType (pos $1) $3 }
-  |     '[' sepBy(Term, ',') ']'       { VecLit (pos $1) $2 }
-  |     '{' sepBy(FieldValue, ',') '}' { RecordValue (pos $1) $2 }
-  | '#' '{' sepBy(FieldType, ',') '}'  { RecordType  (pos $1) $3 }
-  | AtomTerm '.' '(' nat ')'           {% mkTupleProj $1 (tokNat (val $4)) }
-
-Ident :: { PosPair Text }
-Ident : ident { fmap (Text.pack . tokIdent) $1 }
-
-IdentRec :: { PosPair Text }
-IdentRec : identrec { fmap (Text.pack . tokRecursor) $1 }
-
-Sort :: { PosPair SortFlags }
-Sort : 'sort'   { fmap (const $ SortFlags False False) $1 }
-     | 'isort'  { fmap (const $ SortFlags True  False) $1 }
-     | 'qsort'  { fmap (const $ SortFlags False True ) $1 }
-     | 'qisort' { fmap (const $ SortFlags True  True ) $1 }
-
-FieldValue :: { (PosPair FieldName, UTerm) }
-FieldValue : Ident '=' Term { ($1, $3) }
-
-FieldType :: { (PosPair FieldName, UTerm) }
-FieldType : Ident ':' LTerm { ($1, $3) }
-
-opt(q) :: { Maybe q }
-  : { Nothing }
-  | q { Just $1 }
+AppTerm :: { UTerm } :
+    AtomTerm                                    { $1 }
+  | AppTerm AtomTerm                            { App $1 $2 }
+
+-- Atomic (base) term
+AtomTerm :: { UTerm } :
+    nat                                         { NatLit (pos $1) (tokNat (val $1)) }
+  | bvlit                                       { BVLit (pos $1) (tokBits (val $1)) }
+  | string                                      { mkString $1 }
+  | Ident                                       { Name $1 }
+  | IdentRec                                    { Recursor Nothing $1 }
+  | 'Prop'                                      { Sort (pos $1) propSort noFlags }
+  | Sort nat                                   { Sort (pos $1) (mkSort (tokNat (val $2))) (val $1) }
+  | AtomTerm '.' Ident                          { RecordProj $1 (val $3) }
+  | AtomTerm '.' IdentRec                       {% parseRecursorProj $1 $3 }
+  | AtomTerm '.' nat                            {% parseTupleSelector $1 (fmap tokNat $3) }
+  | '(' sepBy(Term, ',') ')'                    { mkTupleValue (pos $1) $2 }
+  | '#' '(' sepBy(Term, ',') ')'                { mkTupleType (pos $1) $3 }
+  |     '[' sepBy(Term, ',') ']'                { VecLit (pos $1) $2 }
+  |     '{' sepBy(FieldValue, ',') '}'          { RecordValue (pos $1) $2 }
+  | '#' '{' sepBy(FieldType, ',') '}'           { RecordType  (pos $1) $3 }
+  | AtomTerm '.' '(' nat ')'                    {% mkTupleProj $1 (tokNat (val $4)) }
+
+-- Identifier (wrapper to extract the text)
+Ident :: { PosPair Text } :
+  rawident                                      { fmap (Text.pack . tokIdent) $1 }
+
+-- Recursor identifier (wrapper to extract the text)
+IdentRec :: { PosPair Text } :
+  rawidentrec                                   { fmap (Text.pack . tokRecursor) $1 }
+
+-- Sort keywords
+Sort :: { PosPair SortFlags } :
+    'sort'                                      { fmap (const $ SortFlags False False) $1 }
+  | 'isort'                                     { fmap (const $ SortFlags True  False) $1 }
+  | 'qsort'                                     { fmap (const $ SortFlags False True ) $1 }
+  | 'qisort'                                    { fmap (const $ SortFlags True  True ) $1 }
+
+-- Value for a record field
+FieldValue :: { (PosPair FieldName, UTerm) } :
+  Ident '=' Term                                { ($1, $3) }
+
+-- Type for a record field
+FieldType :: { (PosPair FieldName, UTerm) } :
+  Ident ':' LTerm                               { ($1, $3) }
+
+
+------------------------------------------------------------
+-- Utility productions
+
+-- optional
+opt(q) :: { Maybe q } :
+    {- empty -}                                 { Nothing }
+  | q                                           { Just $1 }
 
 -- Two elements p and r separated by q and terminated by s
-sepPair(p,q,r,s) :: { (p,r) }
-  : p q r s { ($1,$3) }
+sepPair(p, q, r, s) :: { (p, r) } :
+  p q r s                                       { ($1, $3) }
 
 -- A possibly-empty list of p's separated by q.
-sepBy(p,q) :: { [p] }
-  : {- empty -} { [] }
-  | sepBy1(p,q) { $1 }
+sepBy(p, q) :: { [p] } :
+    {- empty -}                                 { [] }
+  | sepBy1(p, q)                                { $1 }
 
--- A possibly-empty list of p's separated by q.
-sepBy1(p,q) :: { [p] }
-  : rsepBy1(p,q) { reverse $1 }
+-- A non-empty list of p's separated by q.
+sepBy1(p, q) :: { [p] } :
+  rsepBy1(p, q)                                 { reverse $1 }
 
-rsepBy1(p,q) :: { [p] }
-  : p { [$1] }
-  | rsepBy1(p,q) q p { $3 : $1 }
+-- A non-empty list of p's separated by q, constructed in reverse order.
+rsepBy1(p, q) :: { [p] } :
+    p                                           { [$1] }
+  | rsepBy1(p, q) q p                           { $3 : $1 }
 
--- A list of 0 or more p's, terminated by q's
-list(p) :: { [p] }
-  : {- empty -} { [] }
-  | rlist1(p) { reverse $1 }
+-- A list of 0 or more p's.
+list(p) :: { [p] } :
+    {- empty -}                                 { [] }
+  | rlist1(p)                                   { reverse $1 }
 
--- A list of 0 or more p's, terminated by q's
-list1(p) :: { [p] }
-  : rlist1(p) { reverse $1 }
+-- A list of 1 or more p's.
+list1(p) :: { [p] } :
+  rlist1(p)                                     { reverse $1 }
 
--- A reversed list of at least 1 p's
-rlist1(p) :: { [p] }
-  : p           { [$1]    }
-  | rlist1(p) p { $2 : $1 }
+-- A list of 1 or more p's, constructed in reverse order.
+rlist1(p) :: { [p] } :
+    p                                           { [$1] }
+  | rlist1(p) p                                 { $2 : $1 }
 
 {
+
 data ParseError
   = UnexpectedLex Text
   | UnexpectedToken Token
@@ -347,9 +369,29 @@ parseTupleSelector t i =
 
 -- | Create a module name given a list of strings with the top-most
 -- module name given first.
+--
+-- The empty list case is impossible according to the grammar.
 mkPosModuleName :: [PosPair Text] -> PosPair ModuleName
-mkPosModuleName [] = error "internal: Unexpected empty module name"
+mkPosModuleName [] = panic "mkPosModuleName" ["Empty module name"]
 mkPosModuleName l = PosPair p (mkModuleName nms)
   where nms = fmap val l
         p = pos (last l)
+
+mkPrimitive :: PosPair Text -> UTerm -> Decl
+mkPrimitive x ty = TypeDecl PrimQualifier x ty
+
+mkAxiom :: PosPair Text -> UTerm -> Decl
+mkAxiom x ty = TypeDecl AxiomQualifier x ty
+
+mkNoQual :: PosPair Text -> UTerm -> Decl
+mkNoQual x ty = TypeDecl NoQualifier x ty
+
+mkInject :: PosPair Token -> PosPair Token -> Decl
+mkInject a b =
+  let fixup t = Text.pack (tokString (val t)) in
+  InjectCodeDecl (fixup a) (fixup b)
+
+mkString :: PosPair Token -> UTerm
+mkString t = StringLit (pos t) (Text.pack (tokString (val t)))
+
 }