src/Pure/Isar/class.ML
changeset 28666 d2dbfe3a0284
parent 28259 5b2af04ec9fb
child 28674 08a77c495dc1
     1.1 --- a/src/Pure/Isar/class.ML	Wed Oct 22 14:15:47 2008 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Oct 22 14:15:48 2008 +0200
     1.3 @@ -40,6 +40,10 @@
     1.4      -> local_theory -> Proof.state
     1.5    val prove_instantiation_instance: (Proof.context -> tactic)
     1.6      -> local_theory -> local_theory
     1.7 +  val prove_instantiation_exit: (Proof.context -> tactic)
     1.8 +    -> local_theory -> theory
     1.9 +  val prove_instantiation_exit_result: (morphism -> 'a -> 'b)
    1.10 +    -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory
    1.11    val conclude_instantiation: local_theory -> local_theory
    1.12    val instantiation_param: local_theory -> string -> string option
    1.13    val confirm_declaration: string -> local_theory -> local_theory
    1.14 @@ -819,6 +823,20 @@
    1.15    fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t
    1.16      (fn {context, ...} => tac context)) ts) lthy) I;
    1.17  
    1.18 +fun prove_instantiation_exit tac = prove_instantiation_instance tac
    1.19 +  #> LocalTheory.exit_global;
    1.20 +
    1.21 +fun prove_instantiation_exit_result f tac x lthy =
    1.22 +  let
    1.23 +    val phi = ProofContext.export_morphism lthy
    1.24 +      (ProofContext.init (ProofContext.theory_of lthy));
    1.25 +    val y = f phi x;
    1.26 +  in
    1.27 +    lthy
    1.28 +    |> prove_instantiation_exit (fn ctxt => tac ctxt y)
    1.29 +    |> pair y
    1.30 +  end;
    1.31 +
    1.32  fun conclude_instantiation lthy =
    1.33    let
    1.34      val { arities, params } = the_instantiation lthy;