src/Pure/Syntax/syntax.ML

       | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
   in
     (case read_asts thy is_logtype syn true root str of
       [ast] => constify ast
     | _ => error ("Syntactically ambiguous input: " ^ quote str))
-  end handle ERROR =>
-    error ("The error(s) above occurred in translation pattern " ^
+  end handle ERROR msg =>
+    cat_error msg ("The error(s) above occurred in translation pattern " ^
       quote str);
 
 
 fun prep_rules rd_pat raw_rules =
   let val rules = map (map_trrule rd_pat) raw_rules in