1.1 --- a/src/Pure/Syntax/syn_trans.ML	Tue Jul 24 19:44:33 2007 +0200
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Tue Jul 24 19:44:35 2007 +0200
     1.3 @@ -491,9 +491,9 @@
     1.4      fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
     1.5        | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
     1.6  
     1.7 -    val exn_results = map (capture ast_of) pts;
     1.8 -    val exns = map_filter get_exn exn_results;
     1.9 -    val results = map_filter get_result exn_results
    1.10 +    val exn_results = map (Exn.capture ast_of) pts;
    1.11 +    val exns = map_filter Exn.get_exn exn_results;
    1.12 +    val results = map_filter Exn.get_result exn_results
    1.13    in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end;
    1.14  
    1.15  
    1.16 @@ -522,9 +522,9 @@
    1.17            | SOME x => Free (x, T))
    1.18          | t => t);
    1.19  
    1.20 -    val exn_results = map (capture (term_of #> free_fixed)) asts;
    1.21 -    val exns = map_filter get_exn exn_results;
    1.22 -    val results = map_filter get_result exn_results
    1.23 +    val exn_results = map (Exn.capture (term_of #> free_fixed)) asts;
    1.24 +    val exns = map_filter Exn.get_exn exn_results;
    1.25 +    val results = map_filter Exn.get_result exn_results
    1.26    in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end;
    1.27  
    1.28  end;