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.
old_header: proper error message;
authorwenzelm
Fri, 08 Oct 1999 17:06:48 +0200
changeset 7810 e5f15a673a69
parent 7809 c3e6f27bfcb7
child 7811 eaf9e022eef3
old_header: proper error message;
src/Pure/Isar/outer_syntax.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/outer_syntax.ML	Fri Oct 08 16:47:44 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Oct 08 17:06:48 1999 +0200
@@ -310,7 +310,8 @@
     || theory_keyword |-- P.!!! theory_header;
 
 val old_header =
-  P.name -- (P.$$$ "=" |-- P.name -- Scan.repeat (P.$$$ "+" |-- P.name))
+  P.!!! (P.group "theory header"
+    (P.name -- (P.$$$ "=" |-- P.name -- Scan.repeat (P.$$$ "+" |-- P.name))))
   >> (fn (A, (B, Bs)) => (A, B :: Bs, []: (string * bool) list));
 
 fun deps_thy name path =
isabelle