--- a/src/Pure/Syntax/syntax.ML Tue Nov 30 10:55:43 1993 +0100
+++ b/src/Pure/Syntax/syntax.ML Tue Nov 30 11:04:07 1993 +0100
@@ -110,12 +110,12 @@
(* empty_tables *)
+(*(* FIXME *)
val empty_tables =
Tabs {
lexicon = empty_lexicon,
roots = [],
- (* gram = empty_gram, *) (* FIXME *)
- gram = mk_gram [] [], (* FIXME *)
+ gram = empty_gram,
consts = [],
parse_ast_trtab = Symtab.null,
parse_ruletab = Symtab.null,
@@ -123,6 +123,7 @@
print_trtab = Symtab.null,
print_ruletab = Symtab.null,
prtab = empty_prtab};
+*)
(* extend_tables *)
@@ -158,6 +159,7 @@
(* mk_tables *)
+(* FIXME *)
(* val mk_tables = extend_tables empty_tables; *)
(* FIXME *)
@@ -426,7 +428,7 @@
val type_syn = mk_syntax (ref (ExtGG (ref EmptyGG, type_ext)));
-(* extend *) (* FIXME *) (* FIXME check *)
+(* extend *) (* FIXME *)
fun old_extend syn read_ty (roots, xconsts, sext) =
let