1.1 --- a/src/HOLCF/Tools/domain/domain_extender.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOLCF/Tools/domain/domain_extender.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -146,6 +146,8 @@
     1.4  
     1.5  local structure P = OuterParse and K = OuterKeyword in
     1.6  
     1.7 +val _ = OuterSyntax.keywords ["lazy"];
     1.8 +
     1.9  val dest_decl =
    1.10    P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
    1.11      (P.name >> SOME) -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1
    1.12 @@ -170,14 +172,10 @@
    1.13    >> (fn (opt_name, doms) =>
    1.14        (case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms));
    1.15  
    1.16 -val domainP =
    1.17 +val _ =
    1.18    OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
    1.19      (domains_decl >> (Toplevel.theory o add_domain));
    1.20  
    1.21 -
    1.22 -val _ = OuterSyntax.add_keywords ["lazy"];
    1.23 -val _ = OuterSyntax.add_parsers [domainP];
    1.24 -
    1.25 -end; (* local structure *)
    1.26 +end;
    1.27  
    1.28  end;