changeset 86 | 2f3a2d9054d1 |
parent 80 | d3d727449d7b |
child 101 | 5f99df1e26c4 |
--- a/ROOT.ML Fri Jun 17 18:34:12 1994 +0200 +++ b/ROOT.ML Mon Jun 20 12:05:03 1994 +0200 @@ -11,7 +11,7 @@ writeln banner; (* Add user section "datatype" *) -use "Datatype"; +use "Datatype.ML"; structure ThySyn = ThySynFun(val user_keywords = ["|", "datatype"] and user_sections = [("datatype", datatype_decls)]); init_thy_reader ();