# HG changeset patch
# User wenzelm
# Date 1216050708 -7200
# Node ID 97ce525f664c7410b82f10dbfc855d64b42febf9
# Parent  75945c8836722644f3321ecab095d5d7ac2ee6b2
end_theory: no result;

diff -r 75945c883672 -r 97ce525f664c src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Jul 14 17:51:47 2008 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Jul 14 17:51:48 2008 +0200
@@ -36,7 +36,7 @@
   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
@@ -526,7 +526,7 @@
     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 *)