--- a/src/Pure/Isar/toplevel.ML Tue Apr 23 11:14:50 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Apr 23 11:14:50 2013 +0200
@@ -110,7 +110,7 @@
(* local theory wrappers *)
val loc_init = Named_Target.context_cmd;
-val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
+val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.assert_nonbrittle #> Local_Theory.exit_global;
fun loc_begin loc (Context.Theory thy) =
(Context.Theory o loc_exit, loc_init (the_default ("-", Position.none) loc) thy)