# HG changeset patch
# User wenzelm
# Date 1337260980 -7200
# Node ID 45a3a1c320d898cdc18aee2f0b7d47fa84a0d5c4
# Parent  7e202f71a24915b224d496a969c9fc6ebeafa18c
tuned error -- reduce potential for confusion in a higher-level context, e.g. partial checking of theory sub-graph;

diff -r 7e202f71a249 -r 45a3a1c320d8 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri May 11 13:41:30 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu May 17 15:23:00 2012 +0200
@@ -188,7 +188,7 @@
   | _ => raise UNDEF);
 
 fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
-  | end_theory pos (State (NONE, _)) = error ("Missing theory" ^ Position.str_of pos)
+  | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.str_of pos)
   | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.str_of pos);