--- a/src/Pure/Isar/toplevel.ML Tue Jul 05 19:45:59 2011 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Jul 05 20:36:49 2011 +0200
@@ -186,7 +186,8 @@
| _ => raise UNDEF);
fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
- | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos);
+ | 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);
(* print state *)