author | nipkow |
Mon, 20 Jun 1994 12:05:03 +0200 | |
changeset 86 | 2f3a2d9054d1 |
parent 85 | 33d50643dccc |
child 87 | b0ea0e55dfe8 |
--- 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 ();