# HG changeset patch # User wenzelm # Date 1394571521 -3600 # Node ID 8fe7414f00b19ba9e88b108591a721a291588d51 # Parent d1130b831e93c7fafe5649d3f61046a459699686 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; diff -r d1130b831e93 -r 8fe7414f00b1 src/Pure/Isar/local_theory.ML --- 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; diff -r d1130b831e93 -r 8fe7414f00b1 src/Pure/Isar/toplevel.ML --- 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)));