# HG changeset patch
# User wenzelm
# Date 1258469615 -3600
# Node ID e2d5d7f51aa335b4529284f4ceec65201a14020a
# Parent  0878aecbf11928d20a487957a6398e5fede81a11
init_theory: Runtime.controlled_execution for proper exception trace etc.;

diff -r 0878aecbf119 -r e2d5d7f51aa3 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Nov 17 14:51:57 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Nov 17 15:53:35 2009 +0100
@@ -302,7 +302,8 @@
 local
 
 fun apply_tr int (Init (_, f, exit)) (State (NONE, _)) =
-      State (SOME (Theory (Context.Theory (Theory.checkpoint (f int)), NONE), exit), NONE)
+      State (SOME (Theory (Context.Theory
+          (Theory.checkpoint (Runtime.controlled_execution f int)), NONE), exit), NONE)
   | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
       State (NONE, prev)
   | apply_tr _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =