diff -r 111ccda5009b -r f025cf787554 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Thu Sep 07 21:21:07 2000 +0200
+++ b/src/Pure/Syntax/printer.ML	Thu Sep 07 22:37:59 2000 +0200
@@ -54,7 +54,7 @@
 fun apply_trans name a fs args =
   (apply_first fs args handle
     Match => raise Match
-  | exn => (writeln ("Error in " ^ name ^ " for " ^ quote a); raise exn));
+  | exn => (priority ("Error in " ^ name ^ " for " ^ quote a); raise exn));
 
 fun apply_typed x y fs = map (fn f => f x y) fs;
 
@@ -308,7 +308,7 @@
     and prefixT (_, a, [], _) = [Pretty.str a]
       | prefixT (c, _, args, p) =
           if c = Ast.Constant "_appl" orelse c = Ast.Constant "_applC" then
-            error "Syntax insufficient for printing prefix applications!"
+            [Pretty.str "*** INSUFFICIENT SYNTAX FOR PREFIX APPLICATION ***"]
           else astT (appT (c, args), p)
 
     and splitT 0 ([x], ys) = (x, ys)