src/Pure/Syntax/syn_trans.ML

--- a/src/Pure/Syntax/syn_trans.ML	Tue Jul 24 19:44:33 2007 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Tue Jul 24 19:44:35 2007 +0200
@@ -491,9 +491,9 @@
     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 (capture ast_of) pts;
-    val exns = map_filter get_exn exn_results;
-    val results = map_filter get_result exn_results
+    val exn_results = map (Exn.capture ast_of) pts;
+    val exns = map_filter Exn.get_exn exn_results;
+    val results = map_filter Exn.get_result exn_results
   in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end;
 
 
@@ -522,9 +522,9 @@
           | SOME x => Free (x, T))
         | t => t);
 
-    val exn_results = map (capture (term_of #> free_fixed)) asts;
-    val exns = map_filter get_exn exn_results;
-    val results = map_filter get_result exn_results
+    val exn_results = map (Exn.capture (term_of #> free_fixed)) asts;
+    val exns = map_filter Exn.get_exn exn_results;
+    val results = map_filter Exn.get_result exn_results
   in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end;
 
 end;