src/Pure/Isar/class_target.ML

   val refresh_syntax: class -> Proof.context -> Proof.context
   val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
 
   (*instances*)
   val init_instantiation: string list * (string * sort) list * sort
-    -> theory -> local_theory
+    -> theory -> Proof.context
   val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
   val instantiation_instance: (local_theory -> local_theory)
     -> local_theory -> Proof.state
   val prove_instantiation_instance: (Proof.context -> tactic)
     -> local_theory -> local_theory