| changeset 223 | 7892b76adb5b |
| parent 57 | 87e14d7f20dc |
| child 241 | a8ff0932d78a |
--- a/src/Pure/Makefile Tue Jan 11 08:10:18 1994 +0100 +++ b/src/Pure/Makefile Tue Jan 11 11:36:32 1994 +0100 @@ -25,7 +25,7 @@ drule.ML tctical.ML tactic.ML goals.ML install_pp.ML SYNTAX_FILES = Syntax/ROOT.ML Syntax/ast.ML Syntax/xgram.ML\ - Syntax/extension.ML Syntax/lexicon.ML Syntax/parse_tree.ML\ + Syntax/extension.ML Syntax/lexicon.ML\ Syntax/parser.ML Syntax/type_ext.ML Syntax/sextension.ML\ Syntax/pretty.ML Syntax/printer.ML Syntax/syntax.ML\ Syntax/earley0A.ML