src/Pure/Isar/toplevel.ML
changeset 68869 3739acbc2178
parent 68839 d8251a61cce8
child 68875 7f0151c951e3
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Sep 01 16:08:54 2018 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Sep 01 17:16:36 2018 +0200
     1.3 @@ -170,8 +170,7 @@
     1.4    | is_end_theory _ = false;
     1.5  
     1.6  fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
     1.7 -  | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos)
     1.8 -  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos);
     1.9 +  | end_theory pos _ = error ("Malformed theory" ^ Position.here pos);
    1.10  
    1.11  
    1.12  (* presentation context *)