--- a/src/Pure/Isar/class.ML Thu Feb 21 09:15:06 2019 +0000
+++ b/src/Pure/Isar/class.ML Thu Feb 21 09:15:07 2019 +0000
@@ -39,6 +39,9 @@
-> string list * (string * sort) list * sort
val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
+ val theory_map_result: string list * (string * sort) list * sort
+ -> (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory)
+ -> (Proof.context -> 'b -> tactic) -> theory -> 'b * theory
(*subclasses*)
val classrel: class * class -> theory -> Proof.state
@@ -749,6 +752,11 @@
|> pair y
end;
+fun theory_map_result arities f g tac =
+ instantiation arities
+ #> g
+ #-> prove_instantiation_exit_result f tac;
+
(* simplified instantiation interface with no class parameter *)