# HG changeset patch
# User wenzelm
# Date 1229023077 -3600
# Node ID b92443a701de7d7a80afc45880a2dd796db15b3b
# Parent  9c98e197a1430534fffcaf9bd0e13b5954abf49e
removed spurious exception_trace;

diff -r 9c98e197a143 -r b92443a701de src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Dec 11 17:32:37 2008 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Dec 11 20:17:57 2008 +0100
@@ -739,7 +739,7 @@
       in (result, st'') end
   end;
 
-fun excursion input = exception_trace (fn () =>
+fun excursion input =
   let
     val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
 
@@ -750,6 +750,6 @@
         State (NONE, SOME (Theory (Context.Theory _, _), _)) => ()
       | _ => error "Unfinished development at end of input");
     val results = maps Lazy.force future_results;
-  in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end);
+  in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end;
 
 end;