src/Pure/Thy/thy_parse.ML
changeset 6022 259e4f2114e1
parent 6015 d1d5dd2f121c
child 6043 3eecc7fbfad8
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Fri Dec 11 10:34:03 1998 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Fri Dec 11 10:36:39 1998 +0100
     1.3 @@ -423,7 +423,8 @@
     1.4  (* locale *)
     1.5  
     1.6  val locale_decl =
     1.7 -  (name --$$ "=") --
     1.8 +  (name --$$ "=") -- 
     1.9 +    (optional ((ident >> (fn x => parens ("Some" ^ quote x))) --$$ "+") ("None")) --
    1.10      ("fixes" $$--
    1.11        (repeat (name --$$ "::" -- !! (typ -- opt_mixfix)) 
    1.12         >> (mk_big_list o map mk_triple2))) --
    1.13 @@ -435,7 +436,7 @@
    1.14       ("defines" $$-- (repeat ((ident >> quote) -- !! string) 
    1.15  		      >> (mk_list o map mk_pair)))
    1.16       "[]")
    1.17 -  >> (fn (((nm, cs), asms), defs) => cat_lines [nm, cs, asms, defs]);
    1.18 +  >> (fn ((((nm, ext), cs), asms), defs) => cat_lines [nm, ext, cs, asms, defs]);
    1.19  
    1.20  
    1.21