clarified Toplevel.end_theory;
authorwenzelm
Sat Aug 13 21:06:01 2011 +0200 (2011-08-13)
changeset 441889e6698b9dcea
parent 44187 88d770052bac
child 44191 be78e13a80d6
clarified Toplevel.end_theory;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Aug 13 20:49:41 2011 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Aug 13 21:06:01 2011 +0200
     1.3 @@ -185,8 +185,8 @@
     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 (SOME _, _)) = error ("Unfinished theory " ^ Position.str_of pos)
     1.8 -  | end_theory pos (State (NONE, NONE)) = error ("Missing theory " ^ Position.str_of pos);
     1.9 +  | end_theory pos (State (NONE, _)) = error ("Missing theory " ^ Position.str_of pos)
    1.10 +  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory " ^ Position.str_of pos);
    1.11  
    1.12  
    1.13  (* print state *)