end_theory: no result;
authorwenzelm
Mon, 14 Jul 2008 17:51:48 +0200
changeset 27579 97ce525f664c
parent 27578 75945c883672
child 27580 e16f4baa3db6
end_theory: no result;
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 *)