src/Pure/Isar/outer_syntax.ML
changeset 7810 e5f15a673a69
parent 7789 57d20133224e
child 7903 cc6177e1efca
     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 =