Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified Toplevel.end_theory;
authorwenzelm
Sat, 13 Aug 2011 21:06:01 +0200
changeset 44188 9e6698b9dcea
parent 44187 88d770052bac
child 44191 be78e13a80d6
clarified Toplevel.end_theory;
src/Pure/Isar/toplevel.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/toplevel.ML	Sat Aug 13 20:49:41 2011 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Aug 13 21:06:01 2011 +0200
@@ -185,8 +185,8 @@
   | _ => raise UNDEF);
 
 fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
-  | 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);
+  | end_theory pos (State (NONE, _)) = error ("Missing theory " ^ Position.str_of pos)
+  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory " ^ Position.str_of pos);
 
 
 (* print state *)
isabelle