replaced TRANSLATION_FAIL by EXCEPTION;

--- a/src/Pure/Syntax/printer.ML	Tue Sep 13 22:19:48 2005 +0200
+++ b/src/Pure/Syntax/printer.ML	Tue Sep 13 22:19:49 2005 +0200
@@ -64,7 +64,7 @@
       | app_first (f :: fs) = f thy args handle Match => app_first fs;
   in
     transform_failure (fn Match => Match
-      | exn => SynTrans.TRANSLATION_FAIL (exn, "Error in " ^ name ^ " for " ^ quote a))
+      | exn => EXCEPTION (exn, "Error in " ^ name ^ " for " ^ quote a))
       app_first fns
   end;
 

--- a/src/Pure/Syntax/syn_trans.ML	Tue Sep 13 22:19:48 2005 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Tue Sep 13 22:19:49 2005 +0200
@@ -21,7 +21,6 @@
   val mark_bound: string -> term
   val mark_boundT: string * typ -> term
   val variant_abs': string * typ * term -> string * term
-  exception TRANSLATION_FAIL of exn * string
 end;
 
 signature SYN_TRANS1 =
@@ -458,15 +457,13 @@
 
 (** pts_to_asts **)
 
-exception TRANSLATION_FAIL of exn * string;
-
 fun pts_to_asts thy trf pts =
   let
     fun trans a args =
       (case trf a of
         NONE => Ast.mk_appl (Ast.Constant a) args
       | SOME f => transform_failure (fn exn =>
-            TRANSLATION_FAIL (exn, "Error in parse ast translation for " ^ quote a))
+            EXCEPTION (exn, "Error in parse ast translation for " ^ quote a))
           (fn () => f thy args) ());
 
     (*translate pt bottom-up*)
@@ -488,7 +485,7 @@
       (case trf a of
         NONE => Term.list_comb (Lexicon.const a, args)
       | SOME f => transform_failure (fn exn =>
-            TRANSLATION_FAIL (exn, "Error in parse translation for " ^ quote a))
+            EXCEPTION (exn, "Error in parse translation for " ^ quote a))
           (fn () => f thy args) ());
 
     fun term_of (Ast.Constant a) = trans a []