# HG changeset patch
# User wenzelm
# Date 1207826653 -7200
# Node ID 791e4b436f8a885ec3678c7e8190fa73f64b05b6
# Parent  1249f49d081921898a1eac52793caa80ccc41a94
Context.set_thread_data: non-critical;

diff -r 1249f49d0819 -r 791e4b436f8a src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 10 13:24:11 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 10 13:24:13 2008 +0200
@@ -318,7 +318,7 @@
 val welcome = Toplevel.imperative (writeln o Session.welcome);
 
 val exit = Toplevel.keep (fn state =>
- (CRITICAL (fn () => Context.set_thread_data (try Toplevel.generic_theory_of state));
+ (Context.set_thread_data (try Toplevel.generic_theory_of state);
   raise Toplevel.TERMINATE));
 
 val quit = Toplevel.imperative quit;