reraise exceptions to preserve position information;

--- a/src/Pure/Syntax/syn_trans.ML	Wed Jun 10 00:46:37 2009 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Wed Jun 10 11:12:06 2009 +0200
@@ -223,7 +223,7 @@
 
 fun the_struct structs i =
   if 1 <= i andalso i <= length structs then nth structs (i - 1)
-  else raise error ("Illegal reference to implicit structure #" ^ string_of_int i);
+  else error ("Illegal reference to implicit structure #" ^ string_of_int i);
 
 fun struct_tr structs (*"_struct"*) [Const ("_indexdefault", _)] =
       Lexicon.free (the_struct structs 1)
@@ -503,7 +503,7 @@
     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;
+  in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
 
 
 
@@ -534,6 +534,6 @@
     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;
+  in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
 
 end;

--- a/src/Pure/Thy/thy_info.ML	Wed Jun 10 00:46:37 2009 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Jun 10 11:12:06 2009 +0200
@@ -387,7 +387,7 @@
     (case Graph.get_node tasks name of
       Task body =>
         let val after_load = body ()
-        in after_load () handle exn => (kill_thy name; raise exn) end
+        in after_load () handle exn => (kill_thy name; reraise exn) end
     | _ => ()));
 
 in