src/Pure/Syntax/syntax.ML
changeset 171 ab0f93a291b5
parent 168 1bf4e2cab673
child 174 319ff2d6760b
     1.1 --- a/src/Pure/Syntax/syntax.ML	Tue Nov 30 10:55:43 1993 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Nov 30 11:04:07 1993 +0100
     1.3 @@ -110,12 +110,12 @@
     1.4  
     1.5  (* empty_tables *)
     1.6  
     1.7 +(*(* FIXME *)
     1.8  val empty_tables =
     1.9    Tabs {
    1.10      lexicon = empty_lexicon,
    1.11      roots = [],
    1.12 -    (* gram = empty_gram, *)    (* FIXME *)
    1.13 -    gram = mk_gram [] [],       (* FIXME *)
    1.14 +    gram = empty_gram,
    1.15      consts = [],
    1.16      parse_ast_trtab = Symtab.null,
    1.17      parse_ruletab = Symtab.null,
    1.18 @@ -123,6 +123,7 @@
    1.19      print_trtab = Symtab.null,
    1.20      print_ruletab = Symtab.null,
    1.21      prtab = empty_prtab};
    1.22 +*)
    1.23  
    1.24  
    1.25  (* extend_tables *)
    1.26 @@ -158,6 +159,7 @@
    1.27  
    1.28  (* mk_tables *)
    1.29  
    1.30 +(* FIXME *)
    1.31  (* val mk_tables = extend_tables empty_tables; *)
    1.32  
    1.33  (* FIXME *)
    1.34 @@ -426,7 +428,7 @@
    1.35  val type_syn = mk_syntax (ref (ExtGG (ref EmptyGG, type_ext)));
    1.36  
    1.37  
    1.38 -(* extend *)  (* FIXME *) (* FIXME check *)
    1.39 +(* extend *)  (* FIXME *)
    1.40  
    1.41  fun old_extend syn read_ty (roots, xconsts, sext) =
    1.42    let