1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Dec 11 17:32:37 2008 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Dec 11 20:17:57 2008 +0100
     1.3 @@ -739,7 +739,7 @@
     1.4        in (result, st'') end
     1.5    end;
     1.6  
     1.7 -fun excursion input = exception_trace (fn () =>
     1.8 +fun excursion input =
     1.9    let
    1.10      val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
    1.11  
    1.12 @@ -750,6 +750,6 @@
    1.13          State (NONE, SOME (Theory (Context.Theory _, _), _)) => ()
    1.14        | _ => error "Unfinished development at end of input");
    1.15      val results = maps Lazy.force future_results;
    1.16 -  in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end);
    1.17 +  in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end;
    1.18  
    1.19  end;