src/ZF/ROOT.ML
changeset 803 4c8333ab3eae
parent 578 efc648d29dd0
child 1069 66efd8f90fbd
     1.1 --- a/src/ZF/ROOT.ML	Fri Dec 16 17:46:02 1994 +0100
     1.2 +++ b/src/ZF/ROOT.ML	Fri Dec 16 18:07:12 1994 +0100
     1.3 @@ -30,16 +30,7 @@
     1.4  
     1.5  (*Add user sections for inductive/datatype definitions*)
     1.6  use     "../Pure/section_utils.ML";
     1.7 -use_thy "Datatype";
     1.8 -structure ThySyn = ThySynFun
     1.9 - (val user_keywords = ["inductive", "coinductive", "datatype", "codatatype", 
    1.10 -		       "and", "|", "<=", "domains", "intrs", "monos", 
    1.11 -		       "con_defs", "type_intrs", "type_elims"] 
    1.12 -  and user_sections = [("inductive",  inductive_decl ""),
    1.13 -		       ("coinductive",  inductive_decl "Co"),
    1.14 -		       ("datatype",  datatype_decl ""),
    1.15 -		       ("codatatype",  datatype_decl "Co")]);
    1.16 -init_thy_reader ();
    1.17 +use     "thy_syntax.ML";
    1.18  
    1.19  use_thy "InfDatatype";
    1.20  use_thy "List";