slightly more rubust (and opportunistic) exit for old-fashioned theory_to_proof, which is used by global 'sublocale' with Named_Target.init but without proper exit;

--- a/src/Pure/Isar/local_theory.ML	Tue Mar 11 18:36:17 2014 +0100
+++ b/src/Pure/Isar/local_theory.ML	Tue Mar 11 21:58:41 2014 +0100
@@ -65,6 +65,7 @@
   val exit_global: local_theory -> theory
   val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
   val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
+  val perhaps_exit_global: Proof.context -> theory
 end;
 
 structure Local_Theory: LOCAL_THEORY =
@@ -313,6 +314,7 @@
   mark_brittle #> activate_nonbrittle dep_morph mixin export;
 
 
+
 (** init and exit **)
 
 (* init *)
@@ -341,4 +343,9 @@
     val phi = standard_morphism lthy thy_ctxt;
   in (f phi x, thy) end;
 
+fun perhaps_exit_global ctxt =
+  if can assert ctxt
+  then exit_global (assert_bottom true ctxt)
+  else Proof_Context.theory_of ctxt;
+
 end;

--- a/src/Pure/Isar/toplevel.ML	Tue Mar 11 18:36:17 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Mar 11 21:58:41 2014 +0100
@@ -534,7 +534,7 @@
 
 fun theory_to_proof f = begin_proof
   (fn _ => fn gthy =>
-    (Context.Theory o Sign.reset_group o Proof_Context.theory_of,
+    (Context.Theory o Sign.reset_group o Local_Theory.perhaps_exit_global,
       (case gthy of
         Context.Theory thy => f (Sign.new_group thy)
       | _ => raise UNDEF)));