src/HOLCF/domain/interface.ML

     Author : David von Oheimb
     Copyright 1995, 1996 TU Muenchen
 
 parser for domain section
 *)
-
-
-structure ThySynData: THY_SYN_DATA = (* overwrites old version of ThySynData !!!!!! *)
-
-struct
 
 local 
   open ThyParse;
   open Domain_Library;
 

   val domain_decl = (enum1 "," (con_typ --$$ "="  -- !! 
 			       (enum1 "|" domain_cons))) 	    >> mk_domain;
   val gen_by_decl = (optional ($$ "finite" >> K true) false) -- 
 		    (enum1 "," (name'   --$$ "by" -- !!
 			       (enum1 "|" name'))) >> mk_gen_by;
+
+  val _ = ThySyn.add_syntax
+    ["lazy", "by", "finite"]
+    [("domain", domain_decl), ("generated", gen_by_decl)]
+
 end; (* local *)
-
-val user_keywords = "lazy"::"by"::"finite"::
-		(**)filter_out (fn s=>s="lazy" orelse s="by" orelse s="finite")(**)
-		    ThySynData.user_keywords;
-val user_sections = ("domain", domain_decl)::("generated", gen_by_decl)::
-		(**)filter_out (fn (s,_)=>s="domain" orelse s="generated")(**)
-		    ThySynData.user_sections;
-end; (* struct *)
-
-structure ThySyn = ThySynFun(ThySynData); (* overwrites old version of ThySyn!!!!!! *)