added Syntax/symbol_font.ML;
authorwenzelm
Mon, 18 Nov 1996 17:27:59 +0100
changeset 2195 e8271379ba4b
parent 2194 63a68a3a8a76
child 2196 1b36ebc70487
added Syntax/symbol_font.ML;
src/Pure/Makefile
--- a/src/Pure/Makefile	Mon Nov 18 16:34:37 1996 +0100
+++ b/src/Pure/Makefile	Mon Nov 18 17:27:59 1996 +0100
@@ -30,7 +30,7 @@
 SYNTAX_FILES =	Syntax/ROOT.ML	Syntax/ast.ML		Syntax/lexicon.ML\
 	Syntax/parser.ML	Syntax/type_ext.ML	Syntax/syn_trans.ML\
 	Syntax/pretty.ML	Syntax/printer.ML	Syntax/syntax.ML\
-	Syntax/syn_ext.ML	Syntax/mixfix.ML
+	Syntax/syn_ext.ML	Syntax/mixfix.ML	Syntax/symbol_font.ML
 
 THY_FILES = Thy/ROOT.ML		Thy/thy_scan.ML		Thy/thy_parse.ML\
 	Thy/thy_syn.ML		Thy/thy_read.ML		Thy/thm_database.ML