src/Pure/Syntax/syn_trans.ML

 fun struct_trfuns structs =
   ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
 
 
 
-exception TRANSLATION of string * exn
-
 (** pts_to_asts **)
+
+exception TRANSLATION of string * exn;
 
 fun pts_to_asts trf pts =
   let
     fun trans a args =
       (case trf a of

 
     (*translate pt bottom-up*)
     fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
       | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
 
-    val exn_results =
-      map (fn pt => Result (ast_of pt) handle exn => Exn exn) pts;
+    val exn_results = map (capture ast_of) pts;
     val exns = mapfilter get_exn exn_results;
     val results = mapfilter get_result exn_results
   in
-    case results of
-      [] => (case exns of
-        TRANSLATION (a, exn) :: _ =>
-          (writeln ("Error in parse ast translation for " ^ quote a); raise exn)
-      | _ => [])
-    | _ => results
+    (case (results, exns) of
+      ([], TRANSLATION (a, exn) :: _) =>
+        (writeln ("Error in parse ast translation for " ^ quote a); raise exn)
+    | _ => results)
   end;
 
 
 
 (** asts_to_terms **)

           trans a (map term_of asts)
       | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
           Term.list_comb (term_of ast, map term_of asts)
       | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
 
-    val exn_results =
-      map (fn t => Result (term_of t) handle exn => Exn exn) asts;
+    val exn_results = map (capture term_of) asts;
     val exns = mapfilter get_exn exn_results;
     val results = mapfilter get_result exn_results
   in
-    case results of
-      [] => (case exns of
-        TRANSLATION (a, exn) :: _ =>
-          (writeln ("Error in parse translation for " ^ quote a); raise exn)
-      | _ => [])
-    | _ => results
+    (case (results, exns) of
+      ([], TRANSLATION (a, exn) :: _) =>
+        (writeln ("Error in parse translation for " ^ quote a); raise exn)
+    | _ => results)
   end;
 
 end;