old_header: proper error message;
authorwenzelm
Fri Oct 08 17:06:48 1999 +0200 (1999-10-08)
changeset 7810e5f15a673a69
parent 7809 c3e6f27bfcb7
child 7811 eaf9e022eef3
old_header: proper error message;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Oct 08 16:47:44 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Oct 08 17:06:48 1999 +0200
     1.3 @@ -310,7 +310,8 @@
     1.4      || theory_keyword |-- P.!!! theory_header;
     1.5  
     1.6  val old_header =
     1.7 -  P.name -- (P.$$$ "=" |-- P.name -- Scan.repeat (P.$$$ "+" |-- P.name))
     1.8 +  P.!!! (P.group "theory header"
     1.9 +    (P.name -- (P.$$$ "=" |-- P.name -- Scan.repeat (P.$$$ "+" |-- P.name))))
    1.10    >> (fn (A, (B, Bs)) => (A, B :: Bs, []: (string * bool) list));
    1.11  
    1.12  fun deps_thy name path =