src/Pure/Isar/local_theory.ML

   val target_morphism: local_theory -> morphism
   val target_naming: local_theory -> NameSpace.naming
   val target_name: local_theory -> bstring -> string
   val init: string -> operations -> Proof.context -> local_theory
   val restore: local_theory -> local_theory
-  val reinit: local_theory -> theory -> local_theory
+  val reinit: local_theory -> local_theory
   val exit: local_theory -> Proof.context
 end;
 
 structure LocalTheory: LOCAL_THEORY =
 struct

     local_theory -> (bstring * thm list) list * local_theory,
   type_syntax: declaration -> local_theory -> local_theory,
   term_syntax: declaration -> local_theory -> local_theory,
   declaration: declaration -> local_theory -> local_theory,
   target_naming: local_theory -> NameSpace.naming,
-  reinit: local_theory -> theory -> local_theory,
+  reinit: local_theory -> local_theory,
   exit: local_theory -> Proof.context};
 
 datatype lthy = LThy of
  {theory_prefix: string,
   operations: operations,