prove_instantiation_exit combinators

--- a/src/Pure/Isar/class.ML	Wed Oct 22 14:15:47 2008 +0200
+++ b/src/Pure/Isar/class.ML	Wed Oct 22 14:15:48 2008 +0200
@@ -40,6 +40,10 @@
     -> local_theory -> Proof.state
   val prove_instantiation_instance: (Proof.context -> tactic)
     -> local_theory -> local_theory
+  val prove_instantiation_exit: (Proof.context -> tactic)
+    -> local_theory -> theory
+  val prove_instantiation_exit_result: (morphism -> 'a -> 'b)
+    -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory
   val conclude_instantiation: local_theory -> local_theory
   val instantiation_param: local_theory -> string -> string option
   val confirm_declaration: string -> local_theory -> local_theory
@@ -819,6 +823,20 @@
   fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t
     (fn {context, ...} => tac context)) ts) lthy) I;
 
+fun prove_instantiation_exit tac = prove_instantiation_instance tac
+  #> LocalTheory.exit_global;
+
+fun prove_instantiation_exit_result f tac x lthy =
+  let
+    val phi = ProofContext.export_morphism lthy
+      (ProofContext.init (ProofContext.theory_of lthy));
+    val y = f phi x;
+  in
+    lthy
+    |> prove_instantiation_exit (fn ctxt => tac ctxt y)
+    |> pair y
+  end;
+
 fun conclude_instantiation lthy =
   let
     val { arities, params } = the_instantiation lthy;