src/ZF/ROOT.ML
changeset 578 efc648d29dd0
parent 532 851df239ac8b
child 803 4c8333ab3eae
--- a/src/ZF/ROOT.ML	Thu Aug 25 10:41:17 1994 +0200
+++ b/src/ZF/ROOT.ML	Thu Aug 25 12:09:21 1994 +0200
@@ -29,6 +29,7 @@
 print_depth 1;
 
 (*Add user sections for inductive/datatype definitions*)
+use     "../Pure/section_utils.ML";
 use_thy "Datatype";
 structure ThySyn = ThySynFun
  (val user_keywords = ["inductive", "coinductive", "datatype", "codatatype",