src/Pure/Syntax/syntax.ML

--- a/src/Pure/Syntax/syntax.ML	Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sat Jan 14 17:14:06 2006 +0100
@@ -447,8 +447,8 @@
     (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);