src/Pure/Thy/thy_info.ML

   val time_use_thy: string -> unit
   val remove_thy: string -> unit
   val kill_thy: string -> unit
   val thy_ord: theory * theory -> order
   val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
-  val end_theory: theory -> theory
+  val end_theory: theory -> unit
   val register_thy: string -> unit
   val register_theory: theory -> unit
   val finish: unit -> unit
 end;
 

   let
     val name = Context.theory_name theory;
     val _ = check_files name;
     val theory' = Theory.end_theory theory;
     val _ = change_thy name (fn (deps, _) => (deps, SOME theory'));
-  in theory' end;
+  in () end;
 
 
 (* register existing theories *)
 
 fun register_thy name =