tuned error -- reduce potential for confusion in a higher-level context, e.g. partial checking of theory sub-graph;
authorwenzelm
Thu May 17 15:23:00 2012 +0200 (2012-05-17)
changeset 4788145a3a1c320d8
parent 47880 7e202f71a249
child 47882 ed5f56b8f90a
tuned error -- reduce potential for confusion in a higher-level context, e.g. partial checking of theory sub-graph;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Fri May 11 13:41:30 2012 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu May 17 15:23:00 2012 +0200
     1.3 @@ -188,7 +188,7 @@
     1.4    | _ => raise UNDEF);
     1.5  
     1.6  fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
     1.7 -  | end_theory pos (State (NONE, _)) = error ("Missing theory" ^ Position.str_of pos)
     1.8 +  | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.str_of pos)
     1.9    | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.str_of pos);
    1.10  
    1.11