# HG changeset patch
# User wenzelm
# Date 1313262361 -7200
# Node ID 9e6698b9dcea204a819a5773fd8d7fe915849d71
# Parent  88d770052bacf2a8d0aa49ae9b6fc873d09851e9
clarified Toplevel.end_theory;

diff -r 88d770052bac -r 9e6698b9dcea src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Aug 13 20:49:41 2011 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Aug 13 21:06:01 2011 +0200
@@ -185,8 +185,8 @@
   | _ => raise UNDEF);
 
 fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
-  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory " ^ Position.str_of pos)
-  | end_theory pos (State (NONE, NONE)) = error ("Missing theory " ^ Position.str_of pos);
+  | end_theory pos (State (NONE, _)) = error ("Missing theory " ^ Position.str_of pos)
+  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory " ^ Position.str_of pos);
 
 
 (* print state *)